This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imbi13

Description: Join three logical equivalences to form equivalence of implications. imbi13 is imbi13VD without virtual deductions and was automatically derived from imbi13VD 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.)

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

Proof

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