(P → Q) ↔ ( ¬P ∨ Q) is the goal, there's no premises
I start with 2.|_ P -> Q..................
3.||_ P......................
4., _ ~P....................
5., |....................RULE: | INTRO 3, 4
6., Q......................RULE: | ELIM 5
7.|| Q.......................RULE: ?
8.| Q........................RULE: ?
9.| ~P V Q...................RULE: V INTRO 8 END 1ST SUBPROOF
10.|_ ~P V Q.................
11.||_ ~P....................
12., _ P....................
13., |...................RULE: | INTRO 11, 12
14., P -> Q................RULE: | ELIM 13
15.|| P ->Q..................RULE: ?
END 1ST ASSUMPTION
16.||_ Q.....................
17., _ ~Q...................
18., |...................RULE: | INTRO 16, 17
19., P -> Q................RULE: | ELIM 18
20.|| P -> Q.................RULE: ? END 2ND ASSUMPTION
21.|P -> Q...................RULE: V ELIM 10, 11-15, 16-20
- (P -> Q) <-> (~P V Q)....RULE: <-> INTRO 2-9, 10-21
This is what I have so far, I am missing a few rules on how it can be apply, if anyone can help :)