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 ( 𝜒𝜑 )