Theorem e12 44135

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

Syntax hints:   → wi 4  (   wvd1 43980  (   wvd2 43988

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 206  df-an 396  df-vd1 43981  df-vd2 43989

This theorem is referenced by:  e12an  44136  trsspwALT  44229  sspwtr  44232  pwtrVD  44235  snssiALTVD  44238  elex2VD  44249  elex22VD  44250  eqsbc2VD  44251  en3lplem1VD  44254  3ornot23VD  44258  orbi1rVD  44259  19.21a3con13vVD  44263  exbirVD  44264  tratrbVD  44272  ssralv2VD  44277  sbcim2gVD  44286  sbcbiVD  44287  relopabVD  44312  19.41rgVD  44313  ax6e2eqVD  44318  ax6e2ndeqVD  44320  vk15.4jVD  44325  con3ALTVD  44327