Theorem imbi12VD 41214

Description: Implication form of imbi12i 353. 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. imbi12 349 is imbi12VD 41214 without virtual deductions and was automatically derived from imbi12VD 41214.

1::	⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)    ▶   (𝜒 ↔ 𝜃)   )
3::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜑 → 𝜒)   )
4:1,3:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜓 → 𝜒)   )
5:2,4:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜓 → 𝜃)   )
6:5:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)    ▶   ((𝜑 → 𝜒) → (𝜓 → 𝜃))   )
7::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜓 → 𝜃)   )
8:1,7:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜑 → 𝜃)   )
9:2,8:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜑 → 𝜒)   )
10:9:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)    ▶   ((𝜓 → 𝜃) → (𝜑 → 𝜒))   )
11:6,10:	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)    ▶   ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))   )
12:11:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))   )
qed:12:	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))

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

Assertion

Ref	Expression
imbi12VD	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))

Proof of Theorem imbi12VD

Step	Hyp	Ref	Expression
1		idn2 40954	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   (𝜒 ↔ 𝜃)   )
2		idn1 40915	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
3		idn3 40956	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜑 → 𝜒)   )
4		biimpr 222	. . . . . . . 8 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
5	4	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) → (𝜓 → 𝜒)))
6	2, 3, 5	e13 41089	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜓 → 𝜒)   )
7		biimp 217	. . . . . . 7 ⊢ ((𝜒 ↔ 𝜃) → (𝜒 → 𝜃))
8	7	imim2d 57	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
9	1, 6, 8	e23 41096	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜓 → 𝜃)   )
10	9	in3 40950	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜑 → 𝜒) → (𝜓 → 𝜃))   )
11		idn3 40956	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜓 → 𝜃)   )
12		biimp 217	. . . . . . . 8 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
13	12	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ↔ 𝜓) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))
14	2, 11, 13	e13 41089	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜑 → 𝜃)   )
15		biimpr 222	. . . . . . 7 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
16	15	imim2d 57	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜃) → (𝜑 → 𝜒)))
17	1, 14, 16	e23 41096	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜑 → 𝜒)   )
18	17	in3 40950	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜓 → 𝜃) → (𝜑 → 𝜒))   )
19		impbi 210	. . . 4 ⊢ (((𝜑 → 𝜒) → (𝜓 → 𝜃)) → (((𝜓 → 𝜃) → (𝜑 → 𝜒)) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
20	10, 18, 19	e22 41012	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))   )
21	20	in2 40946	. 2 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))   )
22	21	in1 40912	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))

Syntax hints:   → wi 4   ↔ wb 208

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 209  df-an 399  df-3an 1085  df-vd1 40911  df-vd2 40919  df-vd3 40931

This theorem is referenced by: (None)