Theorem 3impexpbicomiVD 45457

Description: Virtual deduction proof of 3impexpbicomi 45081. 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.

h1::	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))
qed:1,?: e0a 45371	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))

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

Hypothesis

Ref	Expression
3impexpbicomiVD.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))

Assertion

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

Proof of Theorem 3impexpbicomiVD

Step	Hyp	Ref	Expression
1		3impexpbicomiVD.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))
2		3impexpbicom 45080	. . 3 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
3	2	biimpi 219	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
4	1, 3	e0a 45371	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by: (None)