Metamath Proof Explorer


Theorem imbi1d

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 17-Sep-2013)

Ref Expression
Hypothesis imbid.1 φ ψ χ
Assertion imbi1d φ ψ θ χ θ

Proof

Step Hyp Ref Expression
1 imbid.1 φ ψ χ
2 1 biimprd φ χ ψ
3 2 imim1d φ ψ θ χ θ
4 1 biimpd φ ψ χ
5 4 imim1d φ χ θ ψ θ
6 3 5 impbid φ ψ θ χ θ