Metamath Proof Explorer


Theorem naim12i

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

Ref Expression
Hypotheses naim12i.1
|- ( ph -> ps )
naim12i.2
|- ( ch -> th )
naim12i.3
|- ( ps -/\ th )
Assertion naim12i
|- ( ph -/\ ch )

Proof

Step Hyp Ref Expression
1 naim12i.1
 |-  ( ph -> ps )
2 naim12i.2
 |-  ( ch -> th )
3 naim12i.3
 |-  ( ps -/\ th )
4 1 3 naim1i
 |-  ( ph -/\ th )
5 2 4 naim2i
 |-  ( ph -/\ ch )