Metamath Proof Explorer


Theorem naim12i

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

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

Proof

Step Hyp Ref Expression
1 naim12i.1 ( 𝜑𝜓 )
2 naim12i.2 ( 𝜒𝜃 )
3 naim12i.3 ( 𝜓𝜃 )
4 1 3 naim1i ( 𝜑𝜃 )
5 2 4 naim2i ( 𝜑𝜒 )