Metamath Proof Explorer


Theorem nabi12i

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

Ref Expression
Hypotheses nabi12i.1 φ ψ
nabi12i.2 χ θ
nabi12i.3 ψ θ
Assertion nabi12i φ χ

Proof

Step Hyp Ref Expression
1 nabi12i.1 φ ψ
2 nabi12i.2 χ θ
3 nabi12i.3 ψ θ
4 1 3 nabi1i φ θ
5 2 4 nabi2i φ χ