Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical equivalence
imbi1d
Metamath Proof Explorer
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
⊢ ( 𝜑 → ( ( 𝜓 → 𝜃 ) ↔ ( 𝜒 → 𝜃 ) ) )