Theorem nanbi 1454

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 994	. . 3 |- ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
2		df-or 385	. . 3 |- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) <-> ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) )
3		df-nan 1448	. . . . 5 |- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
4	3	bicomi 214	. . . 4 |- ( -. ( ph /\ ps ) <-> ( ph -/\ ps ) )
5		nannot 1453	. . . . 5 |- ( -. ph <-> ( ph -/\ ph ) )
6		nannot 1453	. . . . 5 |- ( -. ps <-> ( ps -/\ ps ) )
7	5, 6	anbi12i 733	. . . 4 |- ( ( -. ph /\ -. ps ) <-> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
8	4, 7	imbi12i 340	. . 3 |- ( ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
9	1, 2, 8	3bitri 286	. 2 |- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
10		nannan 1451	. 2 |- ( ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
11	9, 10	bitr4i 267	1 |- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   -/\ wnan 1447

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 197  df-or 385  df-an 386  df-nan 1448

This theorem is referenced by:  nic-dfim  1594  nic-dfneg  1595