Metamath Proof Explorer


Theorem naim2i

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

Ref Expression
Hypotheses naim2i.1 φ ψ
naim2i.2 χ ψ
Assertion naim2i χ φ

Proof

Step Hyp Ref Expression
1 naim2i.1 φ ψ
2 naim2i.2 χ ψ
3 naim2 φ ψ χ ψ χ φ
4 1 2 3 mp2 χ φ