Metamath Proof Explorer

Theorem anbi2d

Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 16-Nov-2013)

Ref Expression
Hypothesis anbid.1 φ ψ χ
Assertion anbi2d φ θ ψ θ χ


Step Hyp Ref Expression
1 anbid.1 φ ψ χ
2 1 a1d φ θ ψ χ
3 2 pm5.32d φ θ ψ θ χ