Theorem nanbi

Description: Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof shortened by Wolf Lammen, 27-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		dfbi3	|- ( ( ph <-> ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) )
2		df-or	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ -. ps ) ) <-> ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) )
3		df-nan	|- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
4	3	bicomi	|- ( -. ( ph /\ ps ) <-> ( ph -/\ ps ) )
5		nannot	|- ( -. ph <-> ( ph -/\ ph ) )
6		nannot	|- ( -. ps <-> ( ps -/\ ps ) )
7	5 6	anbi12i	|- ( ( -. ph /\ -. ps ) <-> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) )
8	4 7	imbi12i	|- ( ( -. ( ph /\ ps ) -> ( -. ph /\ -. ps ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
9	1 2 8	3bitri	|- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
10		nannan	|- ( ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) <-> ( ( ph -/\ ps ) -> ( ( ph -/\ ph ) /\ ( ps -/\ ps ) ) ) )
11	9 10	bitr4i	|- ( ( ph <-> ps ) <-> ( ( ph -/\ ps ) -/\ ( ( ph -/\ ph ) -/\ ( ps -/\ ps ) ) ) )