Theorem exbiriVD 45595

Description: Virtual deduction proof of exbiri 823. 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 45436	⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
6:3,5,?: e21 45471	⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
7:4,6,?: e32 45499	⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 45357	. . . . 5 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2		idn2 45355	. . . . . 6 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
3		idn1 45316	. . . . . . 7 ⊢ (   𝜑   ▶   𝜑   )
4		exbiriVD.1	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
5		pm3.3 454	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))))
6	5	com12 33	. . . . . . 7 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜓 → (𝜒 ↔ 𝜃))))
7	3, 4, 6	e10 45436	. . . . . 6 ⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
8		pm2.27 43	. . . . . 6 ⊢ (𝜓 → ((𝜓 → (𝜒 ↔ 𝜃)) → (𝜒 ↔ 𝜃)))
9	2, 7, 8	e21 45471	. . . . 5 ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
10		biimpr 223	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
11	10	com12 33	. . . . 5 ⊢ (𝜃 → ((𝜒 ↔ 𝜃) → 𝜒))
12	1, 9, 11	e32 45499	. . . 4 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
13	12	in3 45351	. . 3 ⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   )
14	13	in2 45347	. 2 ⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   )
15	14	in1 45313	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

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 45312  df-vd2 45320  df-vd3 45332

This theorem is used by: (None)