Metamath Proof Explorer


Theorem nabi12i

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

Ref Expression
Hypotheses nabi12i.1 ( 𝜑𝜓 )
nabi12i.2 ( 𝜒𝜃 )
nabi12i.3 ( 𝜓𝜃 )
Assertion nabi12i ( 𝜑𝜒 )

Proof

Step Hyp Ref Expression
1 nabi12i.1 ( 𝜑𝜓 )
2 nabi12i.2 ( 𝜒𝜃 )
3 nabi12i.3 ( 𝜓𝜃 )
4 1 3 nabi1i ( 𝜑𝜃 )
5 2 4 nabi2i ( 𝜑𝜒 )