Theorem e12 45168

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

Syntax hints:   → wi 4  (   wvd1 45014  (   wvd2 45022

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 45015  df-vd2 45023

This theorem is referenced by:  e12an  45169  trsspwALT  45262  sspwtr  45265  pwtrVD  45268  snssiALTVD  45271  elex2VD  45282  elex22VD  45283  eqsbc2VD  45284  en3lplem1VD  45287  3ornot23VD  45291  orbi1rVD  45292  19.21a3con13vVD  45296  exbirVD  45297  tratrbVD  45305  ssralv2VD  45310  sbcim2gVD  45319  sbcbiVD  45320  relopabVD  45345  19.41rgVD  45346  ax6e2eqVD  45351  ax6e2ndeqVD  45353  vk15.4jVD  45358  con3ALTVD  45360