Theorem e1a 43902

Description: A Virtual deduction elimination rule. syl 17 is e1a 43902 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e1a.1	⊢ (   𝜑   ▶   𝜓   )
e1a.2	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
e1a	⊢ (   𝜑   ▶   𝜒   )

Proof of Theorem e1a

Step	Hyp	Ref	Expression
1		e1a.1	. . . 4 ⊢ (   𝜑   ▶   𝜓   )
2	1	in1 43846	. . 3 ⊢ (𝜑 → 𝜓)
3		e1a.2	. . 3 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → 𝜒)
5	4	dfvd1ir 43848	1 ⊢ (   𝜑   ▶   𝜒   )

Syntax hints:   → wi 4  (   wvd1 43844

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-vd1 43845

This theorem is referenced by:  e1bi  43904  e1bir  43905  snelpwrVD  44106  unipwrVD  44107  sstrALT2VD  44109  elex2VD  44113  elex22VD  44114  eqsbc2VD  44115  zfregs2VD  44116  tpid3gVD  44117  en3lplem1VD  44118  en3lpVD  44120  3ornot23VD  44122  3orbi123VD  44125  sbc3orgVD  44126  exbirVD  44128  3impexpVD  44131  3impexpbicomVD  44132  tratrbVD  44136  al2imVD  44137  syl5impVD  44138  ssralv2VD  44141  ordelordALTVD  44142  sbcim2gVD  44150  trsbcVD  44152  truniALTVD  44153  trintALTVD  44155  undif3VD  44157  sbcssgVD  44158  csbingVD  44159  onfrALTlem3VD  44162  simplbi2comtVD  44163  onfrALTlem2VD  44164  onfrALTVD  44166  csbeq2gVD  44167  csbsngVD  44168  csbxpgVD  44169  csbresgVD  44170  csbrngVD  44171  csbima12gALTVD  44172  csbunigVD  44173  csbfv12gALTVD  44174  con5VD  44175  relopabVD  44176  19.41rgVD  44177  2pm13.193VD  44178  hbimpgVD  44179  hbalgVD  44180  hbexgVD  44181  ax6e2eqVD  44182  ax6e2ndVD  44183  ax6e2ndeqVD  44184  2sb5ndVD  44185  2uasbanhVD  44186  e2ebindVD  44187  sb5ALTVD  44188  vk15.4jVD  44189  notnotrALTVD  44190  con3ALTVD  44191