Theorem e1a 44639

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

Syntax hints:   → wi 4  (   wvd1 44581

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

This theorem is referenced by:  e1bi  44641  e1bir  44642  snelpwrVD  44842  unipwrVD  44843  sstrALT2VD  44845  elex2VD  44849  elex22VD  44850  eqsbc2VD  44851  zfregs2VD  44852  tpid3gVD  44853  en3lplem1VD  44854  en3lpVD  44856  3ornot23VD  44858  3orbi123VD  44861  sbc3orgVD  44862  exbirVD  44864  3impexpVD  44867  3impexpbicomVD  44868  tratrbVD  44872  al2imVD  44873  syl5impVD  44874  ssralv2VD  44877  ordelordALTVD  44878  sbcim2gVD  44886  trsbcVD  44888  truniALTVD  44889  trintALTVD  44891  undif3VD  44893  sbcssgVD  44894  csbingVD  44895  onfrALTlem3VD  44898  simplbi2comtVD  44899  onfrALTlem2VD  44900  onfrALTVD  44902  csbeq2gVD  44903  csbsngVD  44904  csbxpgVD  44905  csbresgVD  44906  csbrngVD  44907  csbima12gALTVD  44908  csbunigVD  44909  csbfv12gALTVD  44910  con5VD  44911  relopabVD  44912  19.41rgVD  44913  2pm13.193VD  44914  hbimpgVD  44915  hbalgVD  44916  hbexgVD  44917  ax6e2eqVD  44918  ax6e2ndVD  44919  ax6e2ndeqVD  44920  2sb5ndVD  44921  2uasbanhVD  44922  e2ebindVD  44923  sb5ALTVD  44924  vk15.4jVD  44925  notnotrALTVD  44926  con3ALTVD  44927