Metamath Proof Explorer

Theorem anbi1d

Description: Deduction adding a right 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 anbi1d φ ψ θ χ θ


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