Theorem e12 44843

Description: A virtual deduction elimination rule (see sylsyld 61). (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 44720	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
3		e12.2	. 2 ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )
4		e12.3	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	2, 3, 4	e22 44791	1 ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )

Syntax hints:   → wi 4  (   wvd1 44689  (   wvd2 44697

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-vd1 44690  df-vd2 44698

This theorem is referenced by:  e12an  44844  trsspwALT  44937  sspwtr  44940  pwtrVD  44943  snssiALTVD  44946  elex2VD  44957  elex22VD  44958  eqsbc2VD  44959  en3lplem1VD  44962  3ornot23VD  44966  orbi1rVD  44967  19.21a3con13vVD  44971  exbirVD  44972  tratrbVD  44980  ssralv2VD  44985  sbcim2gVD  44994  sbcbiVD  44995  relopabVD  45020  19.41rgVD  45021  ax6e2eqVD  45026  ax6e2ndeqVD  45028  vk15.4jVD  45033  con3ALTVD  45035