Theorem e12 45259

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

Syntax hints:   → wi 4  (   wvd1 45105  (   wvd2 45113

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 209  df-an 400  df-vd1 45106  df-vd2 45114

This theorem is referenced by:  e12an  45260  trsspwALT  45353  sspwtr  45356  pwtrVD  45359  snssiALTVD  45362  elex2VD  45373  elex22VD  45374  eqsbc2VD  45375  en3lplem1VD  45378  3ornot23VD  45382  orbi1rVD  45383  19.21a3con13vVD  45387  exbirVD  45388  tratrbVD  45396  ssralv2VD  45401  sbcim2gVD  45410  sbcbiVD  45411  relopabVD  45436  19.41rgVD  45437  ax6e2eqVD  45442  ax6e2ndeqVD  45444  vk15.4jVD  45449  con3ALTVD  45451