Theorem e12 45800

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 45677	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 45748	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

This proof depends on syntax axioms:   → wi 4  (   wvd1 45646  (   wvd2 45654

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 45647  df-vd2 45655

This theorem is used by:  e12an  45801  trsspwALT  45894  sspwtr  45897  pwtrVD  45900  snssiALTVD  45903  elex2VD  45914  elex22VD  45915  eqsbc2VD  45916  en3lplem1VD  45919  3ornot23VD  45923  orbi1rVD  45924  19.21a3con13vVD  45928  exbirVD  45929  tratrbVD  45937  ssralv2VD  45942  sbcim2gVD  45951  sbcbiVD  45952  relopabVD  45977  19.41rgVD  45978  ax6e2eqVD  45983  ax6e2ndeqVD  45985  vk15.4jVD  45990  con3ALTVD  45992