Theorem 3impexpbicomVD 44882

Description: Virtual deduction proof of 3impexpbicom 44505. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
2::	⊢ ((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃))
3:1,2,?: e10 44719	⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
4:3,?: e1a 44652	⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
5:4:	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
6::	⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
7:6,?: e1a 44652	⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
8:7,2,?: e10 44719	⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
9:8:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))
qed:5,9,?: e00 44793	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
3impexpbicomVD	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

Proof of Theorem 3impexpbicomVD

Step	Hyp	Ref	Expression
1		idn1 44599	. . . . 5 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
2		bicom 222	. . . . 5 ⊢ ((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃))
3		imbi2 348	. . . . . 6 ⊢ (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))))
4	3	biimpcd 249	. . . . 5 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))))
5	1, 2, 4	e10 44719	. . . 4 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
6		3impexp 1358	. . . . 5 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
7	6	biimpi 216	. . . 4 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
8	5, 7	e1a 44652	. . 3 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
9	8	in1 44596	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
10		idn1 44599	. . . . 5 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
11	6	biimpri 228	. . . . 5 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)))
12	10, 11	e1a 44652	. . . 4 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
13	3	biimprcd 250	. . . 4 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) → (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))))
14	12, 2, 13	e10 44719	. . 3 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
15	14	in1 44596	. 2 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))
16		impbi 208	. 2 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) → (((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))))
17	9, 15, 16	e00 44793	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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  df-an 396  df-3an 1088  df-vd1 44595

This theorem is referenced by: (None)