Theorem imbi13VD 45660

Description: Join three logical equivalences to form equivalence of implications. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 45307 is imbi13VD 45660 without virtual deductions and was automatically derived from imbi13VD 45660.

1::	⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)    ▶   (𝜒 ↔ 𝜃)   )
3::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜏 ↔ 𝜂)   ▶   (𝜏 ↔ 𝜂)   )
4:2,3:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜏 ↔ 𝜂)   ▶   ((𝜒 → 𝜏) ↔ (𝜃 → 𝜂))   )
5:1,4:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜏 ↔ 𝜂)   ▶   ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))   )
6:5:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)    ▶   ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))   )
7:6:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))))   )
qed:7:	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))))

(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem imbi13VD

Step	Hyp	Ref	Expression
1		idn1 45361	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2		idn2 45400	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   (𝜒 ↔ 𝜃)   )
3		idn3 45402	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜏 ↔ 𝜂)   ▶   (𝜏 ↔ 𝜂)   )
4		imbi12 349	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜒 → 𝜏) ↔ (𝜃 → 𝜂))))
5	2, 3, 4	e23 45541	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜏 ↔ 𝜂)   ▶   ((𝜒 → 𝜏) ↔ (𝜃 → 𝜂))   )
6		imbi12 349	. . . . 5 ⊢ ((𝜑 ↔ 𝜓) → (((𝜒 → 𝜏) ↔ (𝜃 → 𝜂)) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))))
7	1, 5, 6	e13 45534	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜏 ↔ 𝜂)   ▶   ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))   )
8	7	in3 45396	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))   )
9	8	in2 45392	. 2 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂)))))   )
10	9	in1 45358	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-vd1 45357  df-vd2 45365  df-vd3 45377

This theorem is used by: (None)