Metamath Proof Explorer


Theorem nabi2i

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

Ref Expression
Hypotheses nabi2i.1 ( 𝜑𝜓 )
nabi2i.2 ( 𝜒𝜓 )
Assertion nabi2i ( 𝜒𝜑 )

Proof

Step Hyp Ref Expression
1 nabi2i.1 ( 𝜑𝜓 )
2 nabi2i.2 ( 𝜒𝜓 )
3 1 bicomi ( 𝜓𝜑 )
4 3 nanbi2i ( ( 𝜒𝜓 ) ↔ ( 𝜒𝜑 ) )
5 2 4 mpbi ( 𝜒𝜑 )