Theorem imbi13 44545

Description: Join three logical equivalences to form equivalence of implications. imbi13 44545 is imbi13VD 44899 without virtual deductions and was automatically derived from imbi13VD 44899 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
imbi13	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))))

Proof of Theorem imbi13

Step	Hyp	Ref	Expression
1		imbi12 346	. 2 ⊢ ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜒 → 𝜏) ↔ (𝜃 → 𝜂))))
2		imbi12 346	. 2 ⊢ ((𝜑 ↔ 𝜓) → (((𝜒 → 𝜏) ↔ (𝜃 → 𝜂)) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))))
3	1, 2	syl9r 78	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  trsbc  44565  trsbcVD  44902