Theorem 3impexpbicomVD 42477

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

(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 42194	. . . . 5 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
2		bicom 221	. . . . 5 ⊢ ((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃))
3		imbi2 349	. . . . . 6 ⊢ (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))))
4	3	biimpcd 248	. . . . 5 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))))
5	1, 2, 4	e10 42314	. . . 4 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
6		3impexp 1357	. . . . 5 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
7	6	biimpi 215	. . . 4 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
8	5, 7	e1a 42247	. . 3 ⊢ (   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
9	8	in1 42191	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
10		idn1 42194	. . . . 5 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   )
11	6	biimpri 227	. . . . 5 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)))
12	10, 11	e1a 42247	. . . 4 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))   )
13	3	biimprcd 249	. . . 4 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃)) → (((𝜃 ↔ 𝜏) ↔ (𝜏 ↔ 𝜃)) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))))
14	12, 2, 13	e10 42314	. . 3 ⊢ (   (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))   ▶   ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))   )
15	14	in1 42191	. 2 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)))
16		impbi 207	. 2 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))) → (((𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))) → ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))) → (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))))
17	9, 15, 16	e00 42388	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088  df-vd1 42190

This theorem is referenced by: (None)