Theorem nic-justlem 1231

Description: Lemma for handling nested 'nand's.

Assertion

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

Proof of Theorem nic-justlem

Step	Hyp	Ref	Expression
1		df-nand 1230	. . . 4 |- ((ch -/\ ps) <-> -. (ch /\ ps))
2	1	anbi2i 538	. . 3 |- ((ph /\ (ch -/\ ps)) <-> (ph /\ -. (ch /\ ps)))
3	2	notbii 204	. 2 |- (-. (ph /\ (ch -/\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
4		df-nand 1230	. 2 |- ((ph -/\ (ch -/\ ps)) <-> -. (ph /\ (ch -/\ ps)))
5		iman 256	. 2 |- ((ph -> (ch /\ ps)) <-> -. (ph /\ -. (ch /\ ps)))
6	3, 4, 5	3bitr4i 200	1 |- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))

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

This theorem is referenced by:  nic-justim 1232  nic-mp 1237  nic-ax 1239  waj-ax 14238  lukshef-ax2 14239  arg-ax 14240

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