Theorem e12 45908

Description: A virtual deduction elimination rule (see sylsyld 62). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e12.1	⊢ (   𝜑   ▶   𝜓   )
e12.2	⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
e12.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
e12	⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Proof of Theorem e12

Step	Hyp	Ref	Expression
1		e12.1	. . 3 ⊢ (   𝜑   ▶   𝜓   )
2	1	vd12 45785	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 45856	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45754  (   wvd2 45762

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-vd1 45755  df-vd2 45763

This theorem is used by:  e12an  45909  trsspwALT  46002  sspwtr  46005  pwtrVD  46008  snssiALTVD  46011  elex2VD  46022  elex22VD  46023  eqsbc2VD  46024  en3lplem1VD  46027  3ornot23VD  46031  orbi1rVD  46032  19.21a3con13vVD  46036  exbirVD  46037  tratrbVD  46045  ssralv2VD  46050  sbcim2gVD  46059  sbcbiVD  46060  relopabVD  46085  19.41rgVD  46086  ax6e2eqVD  46091  ax6e2ndeqVD  46093  vk15.4jVD  46098  con3ALTVD  46100