Theorem nanbi 1388

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 901	. . 3 |- ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
2		df-or 371	. . 3 |- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) <-> ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) )
3		df-nan 1380	. . . . 5 |- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
4	3	bicomi 205	. . . 4 |- ( -. ( ph /\ ps ) <-> ( ph -/\ ps ) )
5		nannot 1387	. . . . 5 |- ( -. ph <-> ( ph -/\ ph ) )
6		nannot 1387	. . . . 5 |- ( -. ps <-> ( ps -/\ ps ) )
7	5, 6	anbi12i 701	. . . 4 |- ( ( -. ph /\ -. ps ) <-> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
8	4, 7	imbi12i 327	. . 3 |- ( ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
9	1, 2, 8	3bitri 274	. 2 |- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
10		nannan 1384	. 2 |- ( ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
11	9, 10	bitr4i 255	1 |- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   -/\ wnan 1379

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 188  df-or 371  df-an 372  df-nan 1380

This theorem is referenced by:  nic-dfim  1548  nic-dfneg  1549