Theorem exbiriVD 45297

Description: Virtual deduction proof of exbiri 816. 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::	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2::	⊢ (   𝜑   ▶   𝜑   )
3::	⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
4::	⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
5:2,1,?: e10 45138	⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
6:3,5,?: e21 45173	⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
7:4,6,?: e32 45201	⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
8:7:	⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   )
9:8:	⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   )
qed:9:	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

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

Hypothesis

Ref	Expression
exbiriVD.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
exbiriVD	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Proof of Theorem exbiriVD

Step	Hyp	Ref	Expression
1		idn3 45059	. . . . 5 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2		idn2 45057	. . . . . 6 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
3		idn1 45018	. . . . . . 7 ⊢ (   𝜑   ▶   𝜑   )
4		exbiriVD.1	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
5		pm3.3 449	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))))
6	5	com12 32	. . . . . . 7 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜓 → (𝜒 ↔ 𝜃))))
7	3, 4, 6	e10 45138	. . . . . 6 ⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
8		pm2.27 42	. . . . . 6 ⊢ (𝜓 → ((𝜓 → (𝜒 ↔ 𝜃)) → (𝜒 ↔ 𝜃)))
9	2, 7, 8	e21 45173	. . . . 5 ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
10		biimpr 221	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
11	10	com12 32	. . . . 5 ⊢ (𝜃 → ((𝜒 ↔ 𝜃) → 𝜒))
12	1, 9, 11	e32 45201	. . . 4 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
13	12	in3 45053	. . 3 ⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   )
14	13	in2 45049	. 2 ⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   )
15	14	in1 45015	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397  df-3an 1094  df-vd1 45014  df-vd2 45022  df-vd3 45034

This theorem is referenced by: (None)