Theorem nanbi 1393

Description: Show equivalence between the biconditional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)

Assertion

Ref	Expression
nanbi	|- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) )

Proof of Theorem nanbi

Step	Hyp	Ref	Expression
1		dfbi3 904	. . 3 |- ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
2		df-or 372	. . 3 |- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) <-> ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) )
3		df-nan 1385	. . . . 5 |- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
4	3	bicomi 206	. . . 4 |- ( -. ( ph /\ ps ) <-> ( ph -/\ ps ) )
5		nannot 1392	. . . . 5 |- ( -. ph <-> ( ph -/\ ph ) )
6		nannot 1392	. . . . 5 |- ( -. ps <-> ( ps -/\ ps ) )
7	5, 6	anbi12i 703	. . . 4 |- ( ( -. ph /\ -. ps ) <-> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
8	4, 7	imbi12i 328	. . 3 |- ( ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
9	1, 2, 8	3bitri 275	. 2 |- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
10		nannan 1389	. 2 |- ( ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
11	9, 10	bitr4i 256	1 |- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   -/\ wnan 1384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-nan 1385

This theorem is referenced by:  nic-dfim  1552  nic-dfneg  1553