Metamath Proof Explorer


Theorem nanbi2

Description: Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011) (Proof shortened by SF, 2-Jan-2018)

Ref Expression
Assertion nanbi2 φ ψ χ φ χ ψ

Proof

Step Hyp Ref Expression
1 nanbi1 φ ψ φ χ ψ χ
2 nancom χ φ φ χ
3 nancom χ ψ ψ χ
4 1 2 3 3bitr4g φ ψ χ φ χ ψ