Metamath Proof Explorer


Theorem nanbi2i

Description: Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018)

Ref Expression
Hypothesis nanbii.1 φ ψ
Assertion nanbi2i χ φ χ ψ

Proof

Step Hyp Ref Expression
1 nanbii.1 φ ψ
2 nanbi2 φ ψ χ φ χ ψ
3 1 2 ax-mp χ φ χ ψ