Theorem e12 45150

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

Syntax hints:   → wi 4  (   wvd1 44996  (   wvd2 45004

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 44997  df-vd2 45005

This theorem is referenced by:  e12an  45151  trsspwALT  45244  sspwtr  45247  pwtrVD  45250  snssiALTVD  45253  elex2VD  45264  elex22VD  45265  eqsbc2VD  45266  en3lplem1VD  45269  3ornot23VD  45273  orbi1rVD  45274  19.21a3con13vVD  45278  exbirVD  45279  tratrbVD  45287  ssralv2VD  45292  sbcim2gVD  45301  sbcbiVD  45302  relopabVD  45327  19.41rgVD  45328  ax6e2eqVD  45333  ax6e2ndeqVD  45335  vk15.4jVD  45340  con3ALTVD  45342