Theorem e12 45076

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

Syntax hints:   → wi 4  (   wvd1 44922  (   wvd2 44930

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 44923  df-vd2 44931

This theorem is referenced by:  e12an  45077  trsspwALT  45170  sspwtr  45173  pwtrVD  45176  snssiALTVD  45179  elex2VD  45190  elex22VD  45191  eqsbc2VD  45192  en3lplem1VD  45195  3ornot23VD  45199  orbi1rVD  45200  19.21a3con13vVD  45204  exbirVD  45205  tratrbVD  45213  ssralv2VD  45218  sbcim2gVD  45227  sbcbiVD  45228  relopabVD  45253  19.41rgVD  45254  ax6e2eqVD  45259  ax6e2ndeqVD  45261  vk15.4jVD  45266  con3ALTVD  45268