Metamath Proof Explorer


Theorem nabi1i

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

Ref Expression
Hypotheses nabi1i.1 φ ψ
nabi1i.2 ψ χ
Assertion nabi1i φ χ

Proof

Step Hyp Ref Expression
1 nabi1i.1 φ ψ
2 nabi1i.2 ψ χ
3 1 bicomi ψ φ
4 3 nanbi1i ψ χ φ χ
5 2 4 mpbi φ χ