Theorem e1a 40967

Description: A Virtual deduction elimination rule. syl 17 is e1a 40967 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 40911	. . 3 ⊢ (𝜑 → 𝜓)
3		e1a.2	. . 3 ⊢ (𝜓 → 𝜒)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → 𝜒)
5	4	dfvd1ir 40913	1 ⊢ (   𝜑   ▶   𝜒   )

Syntax hints:   → wi 4  (   wvd1 40909

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

This theorem is referenced by:  e1bi  40969  e1bir  40970  snelpwrVD  41171  unipwrVD  41172  sstrALT2VD  41174  elex2VD  41178  elex22VD  41179  eqsbc3rVD  41180  zfregs2VD  41181  tpid3gVD  41182  en3lplem1VD  41183  en3lpVD  41185  3ornot23VD  41187  3orbi123VD  41190  sbc3orgVD  41191  exbirVD  41193  3impexpVD  41196  3impexpbicomVD  41197  tratrbVD  41201  al2imVD  41202  syl5impVD  41203  ssralv2VD  41206  ordelordALTVD  41207  sbcim2gVD  41215  trsbcVD  41217  truniALTVD  41218  trintALTVD  41220  undif3VD  41222  sbcssgVD  41223  csbingVD  41224  onfrALTlem3VD  41227  simplbi2comtVD  41228  onfrALTlem2VD  41229  onfrALTVD  41231  csbeq2gVD  41232  csbsngVD  41233  csbxpgVD  41234  csbresgVD  41235  csbrngVD  41236  csbima12gALTVD  41237  csbunigVD  41238  csbfv12gALTVD  41239  con5VD  41240  relopabVD  41241  19.41rgVD  41242  2pm13.193VD  41243  hbimpgVD  41244  hbalgVD  41245  hbexgVD  41246  ax6e2eqVD  41247  ax6e2ndVD  41248  ax6e2ndeqVD  41249  2sb5ndVD  41250  2uasbanhVD  41251  e2ebindVD  41252  sb5ALTVD  41253  vk15.4jVD  41254  notnotrALTVD  41255  con3ALTVD  41256