Theorem imbi12VD 42382

Description: Implication form of imbi12i 350. 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 346 is imbi12VD 42382 without virtual deductions and was automatically derived from imbi12VD 42382.

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 42122	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   (𝜒 ↔ 𝜃)   )
2		idn1 42083	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
3		idn3 42124	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜑 → 𝜒)   )
4		biimpr 219	. . . . . . . 8 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
5	4	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) → (𝜓 → 𝜒)))
6	2, 3, 5	e13 42257	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜓 → 𝜒)   )
7		biimp 214	. . . . . . 7 ⊢ ((𝜒 ↔ 𝜃) → (𝜒 → 𝜃))
8	7	imim2d 57	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
9	1, 6, 8	e23 42264	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜑 → 𝜒)   ▶   (𝜓 → 𝜃)   )
10	9	in3 42118	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜑 → 𝜒) → (𝜓 → 𝜃))   )
11		idn3 42124	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜓 → 𝜃)   )
12		biimp 214	. . . . . . . 8 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
13	12	imim1d 82	. . . . . . 7 ⊢ ((𝜑 ↔ 𝜓) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))
14	2, 11, 13	e13 42257	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜑 → 𝜃)   )
15		biimpr 219	. . . . . . 7 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
16	15	imim2d 57	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜃) → (𝜑 → 𝜒)))
17	1, 14, 16	e23 42264	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ,   (𝜓 → 𝜃)   ▶   (𝜑 → 𝜒)   )
18	17	in3 42118	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜓 → 𝜃) → (𝜑 → 𝜒))   )
19		impbi 207	. . . 4 ⊢ (((𝜑 → 𝜒) → (𝜓 → 𝜃)) → (((𝜓 → 𝜃) → (𝜑 → 𝜒)) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))
20	10, 18, 19	e22 42180	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ↔ 𝜃)   ▶   ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))   )
21	20	in2 42114	. 2 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))   )
22	21	in1 42080	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))))

Syntax hints:   → wi 4   ↔ wb 205

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 206  df-an 396  df-3an 1087  df-vd1 42079  df-vd2 42087  df-vd3 42099

This theorem is referenced by: (None)