Theorem exbiriVD 42363

Description: Virtual deduction proof of exbiri 807. 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 42203	⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
6:3,5,?: e21 42239	⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
7:4,6,?: e32 42267	⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 42124	. . . . 5 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2		idn2 42122	. . . . . 6 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
3		idn1 42083	. . . . . . 7 ⊢ (   𝜑   ▶   𝜑   )
4		exbiriVD.1	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
5		pm3.3 448	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))))
6	5	com12 32	. . . . . . 7 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜓 → (𝜒 ↔ 𝜃))))
7	3, 4, 6	e10 42203	. . . . . 6 ⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
8		pm2.27 42	. . . . . 6 ⊢ (𝜓 → ((𝜓 → (𝜒 ↔ 𝜃)) → (𝜒 ↔ 𝜃)))
9	2, 7, 8	e21 42239	. . . . 5 ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
10		biimpr 219	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
11	10	com12 32	. . . . 5 ⊢ (𝜃 → ((𝜒 ↔ 𝜃) → 𝜒))
12	1, 9, 11	e32 42267	. . . 4 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
13	12	in3 42118	. . 3 ⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   )
14	13	in2 42114	. 2 ⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   )
15	14	in1 42080	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396  df-3an 1087  df-vd1 42079  df-vd2 42087  df-vd3 42099

This theorem is referenced by: (None)