Metamath Proof Explorer


Theorem nabi12i

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

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

Proof

Step Hyp Ref Expression
1 nabi12i.1
 |-  ( ph <-> ps )
2 nabi12i.2
 |-  ( ch <-> th )
3 nabi12i.3
 |-  ( ps -/\ th )
4 1 3 nabi1i
 |-  ( ph -/\ th )
5 2 4 nabi2i
 |-  ( ph -/\ ch )