I'm having a little trouble with the following derivation.


Derive:
[P∧(G≡(A∧B))]V(~CVE)
1.B⊃(E⊃F) ASS
2. A
⊃(C⊃D) ASS
3. A V B ASS
4. ~D ~F ASS

I'm assuming that since there are meta-variables in the left disjunct that aren't in the premises, we are going to be using disjunction introduction to introduce them. However, I'm still not sure how to derive (~CV~E). I've tried a couple other things but they lead to dead ends. Does anyone have a hint to get me started? Thanks!