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 ( 𝜑 → ( ( 𝜓𝜃 ) ↔ ( 𝜒𝜃 ) ) )