Metamath Proof Explorer


Theorem nabi1i

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

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

Proof

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