Theorem 3impexpbicomVD 45824

Description: Virtual deduction proof of 3impexpbicom 45448. 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 45662	⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
4:3,?: e1a 45595	⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
5:4:	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
6::	⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
7:6,?: e1a 45595	⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
8:7,2,?: e10 45662	⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
9:8:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))
qed:5,9,?: e00 45735	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

(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 45542	. . . . 5 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
2		bicom 225	. . . . 5 ⊢ ((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃))
3		imbi2 351	. . . . . 6 ⊢ (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))))
4	3	biimpcd 252	. . . . 5 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))))
5	1, 2, 4	e10 45662	. . . 4 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
6		3impexp 1377	. . . . 5 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
7	6	biimpi 219	. . . 4 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
8	5, 7	e1a 45595	. . 3 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
9	8	in1 45539	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
10		idn1 45542	. . . . 5 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
11	6	biimpri 231	. . . . 5 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)))
12	10, 11	e1a 45595	. . . 4 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
13	3	biimprcd 253	. . . 4 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) → (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))))
14	12, 2, 13	e10 45662	. . 3 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
15	14	in1 45539	. 2 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))
16		impbi 211	. 2 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) → (((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))))
17	9, 15, 16	e00 45735	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

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

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 45538

This theorem is used by: (None)