Theorem naim2i 14137

Description: Constructor rule for -/\.

Hypotheses

Ref	Expression
naim2i.1	|- (ph -> ps)
naim2i.2	|- (ch -/\ ps)

Assertion

Ref	Expression
naim2i	|- (ch -/\ ph)

Proof of Theorem naim2i

Step	Hyp	Ref	Expression
1		naim2i.1	. 2 |- (ph -> ps)
2		naim2i.2	. 2 |- (ch -/\ ps)
3		naim2 14135	. 2 |- ((ph -> ps) -> ((ch -/\ ps) -> (ch -/\ ph)))
4	1, 2, 3	mp2 54	1 |- (ch -/\ ph)

Syntax hints:   -> wi 3   -/\ wnand 1229

This theorem is referenced by:  naim12i 14138

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-or 241  df-an 242  df-nand 1230

Copyright terms: Public domain