Metamath Proof Explorer


Theorem nabi1i

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

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

Proof

Step Hyp Ref Expression
1 nabi1i.1
 |-  ( ph <-> ps )
2 nabi1i.2
 |-  ( ps -/\ ch )
3 1 bicomi
 |-  ( ps <-> ph )
4 3 nanbi1i
 |-  ( ( ps -/\ ch ) <-> ( ph -/\ ch ) )
5 2 4 mpbi
 |-  ( ph -/\ ch )