Theorem nabi2 14140

Description: Constructor theorem for -/\.

Assertion

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

Proof of Theorem nabi2

Step	Hyp	Ref	Expression
1		simpl 346	. . . 4 |- (((ph <-> ps) /\ (ph <-> ps)) -> (ph <-> ps))
2	1	anbi2d 678	. . 3 |- (((ph <-> ps) /\ (ph <-> ps)) -> ((ch /\ ph) <-> (ch /\ ps)))
3	2	anidms 480	. 2 |- ((ph <-> ps) -> ((ch /\ ph) <-> (ch /\ ps)))
4		notbi 581	. . 3 |- (((ch /\ ph) <-> (ch /\ ps)) <-> (-. (ch /\ ph) <-> -. (ch /\ ps)))
5	4	biimpi 168	. 2 |- (((ch /\ ph) <-> (ch /\ ps)) -> (-. (ch /\ ph) <-> -. (ch /\ ps)))
6		df-nand 1230	. . . 4 |- ((ch -/\ ph) <-> -. (ch /\ ph))
7		df-nand 1230	. . . 4 |- ((ch -/\ ps) <-> -. (ch /\ ps))
8	6, 7	bibi12i 672	. . 3 |- (((ch -/\ ph) <-> (ch -/\ ps)) <-> (-. (ch /\ ph) <-> -. (ch /\ ps)))
9	8	biimpri 169	. 2 |- ((-. (ch /\ ph) <-> -. (ch /\ ps)) -> ((ch -/\ ph) <-> (ch -/\ ps)))
10	3, 5, 9	3syl 24	1 |- ((ph <-> ps) -> ((ch -/\ ph) <-> (ch -/\ ps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   -/\ wnand 1229

This theorem is referenced by:  nabi2i 14142

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-nand 1230

Copyright terms: Public domain