Metamath Proof Explorer


Theorem nabi2i

Description: Constructor rule for -/\ . (Contributed by Anthony Hart, 2-Sep-2011)

Ref Expression
Hypotheses nabi2i.1
|- ( ph <-> ps )
nabi2i.2
|- ( ch -/\ ps )
Assertion nabi2i
|- ( ch -/\ ph )

Proof

Step Hyp Ref Expression
1 nabi2i.1
 |-  ( ph <-> ps )
2 nabi2i.2
 |-  ( ch -/\ ps )
3 1 bicomi
 |-  ( ps <-> ph )
4 3 nanbi2i
 |-  ( ( ch -/\ ps ) <-> ( ch -/\ ph ) )
5 2 4 mpbi
 |-  ( ch -/\ ph )