Theorem exbiriVD 44852

Description: Virtual deduction proof of exbiri 811. 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 44692	⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
6:3,5,?: e21 44728	⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
7:4,6,?: e32 44756	⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 44613	. . . . 5 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2		idn2 44611	. . . . . 6 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
3		idn1 44572	. . . . . . 7 ⊢ (   𝜑   ▶   𝜑   )
4		exbiriVD.1	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
5		pm3.3 448	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))))
6	5	com12 32	. . . . . . 7 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜓 → (𝜒 ↔ 𝜃))))
7	3, 4, 6	e10 44692	. . . . . 6 ⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
8		pm2.27 42	. . . . . 6 ⊢ (𝜓 → ((𝜓 → (𝜒 ↔ 𝜃)) → (𝜒 ↔ 𝜃)))
9	2, 7, 8	e21 44728	. . . . 5 ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
10		biimpr 220	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
11	10	com12 32	. . . . 5 ⊢ (𝜃 → ((𝜒 ↔ 𝜃) → 𝜒))
12	1, 9, 11	e32 44756	. . . 4 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
13	12	in3 44607	. . 3 ⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   )
14	13	in2 44603	. 2 ⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   )
15	14	in1 44569	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396  df-3an 1088  df-vd1 44568  df-vd2 44576  df-vd3 44588

This theorem is referenced by: (None)