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 φ χ