Metamath Proof Explorer


Theorem naim1i

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

Ref Expression
Hypotheses naim1i.1 ( 𝜑𝜓 )
naim1i.2 ( 𝜓𝜒 )
Assertion naim1i ( 𝜑𝜒 )

Proof

Step Hyp Ref Expression
1 naim1i.1 ( 𝜑𝜓 )
2 naim1i.2 ( 𝜓𝜒 )
3 naim1 ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) )
4 1 2 3 mp2 ( 𝜑𝜒 )