Theorem exbiriVD 45545

Description: Virtual deduction proof of exbiri 822. 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 45386	⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
6:3,5,?: e21 45421	⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
7:4,6,?: e32 45449	⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 45307	. . . . 5 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2		idn2 45305	. . . . . 6 ⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
3		idn1 45266	. . . . . . 7 ⊢ (   𝜑   ▶   𝜑   )
4		exbiriVD.1	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
5		pm3.3 453	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))))
6	5	com12 33	. . . . . . 7 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜓 → (𝜒 ↔ 𝜃))))
7	3, 4, 6	e10 45386	. . . . . 6 ⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   )
8		pm2.27 43	. . . . . 6 ⊢ (𝜓 → ((𝜓 → (𝜒 ↔ 𝜃)) → (𝜒 ↔ 𝜃)))
9	2, 7, 8	e21 45421	. . . . 5 ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   )
10		biimpr 223	. . . . . 6 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 → 𝜒))
11	10	com12 33	. . . . 5 ⊢ (𝜃 → ((𝜒 ↔ 𝜃) → 𝜒))
12	1, 9, 11	e32 45449	. . . 4 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
13	12	in3 45301	. . 3 ⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   )
14	13	in2 45297	. 2 ⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   )
15	14	in1 45263	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 1105  df-vd1 45262  df-vd2 45270  df-vd3 45282

This theorem is referenced by: (None)