This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ ↔ ψ → χ ⊼ φ ↔ χ ⊼ ψ