Theorem e12 45174

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

Syntax hints:   → wi 4  (   wvd1 45020  (   wvd2 45028

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 208  df-an 397  df-vd1 45021  df-vd2 45029

This theorem is referenced by:  e12an  45175  trsspwALT  45268  sspwtr  45271  pwtrVD  45274  snssiALTVD  45277  elex2VD  45288  elex22VD  45289  eqsbc2VD  45290  en3lplem1VD  45293  3ornot23VD  45297  orbi1rVD  45298  19.21a3con13vVD  45302  exbirVD  45303  tratrbVD  45311  ssralv2VD  45316  sbcim2gVD  45325  sbcbiVD  45326  relopabVD  45351  19.41rgVD  45352  ax6e2eqVD  45357  ax6e2ndeqVD  45359  vk15.4jVD  45364  con3ALTVD  45366