Theorem e1a 44666

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

Syntax hints:   → wi 4  (   wvd1 44608

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 44609

This theorem is referenced by:  e1bi  44668  e1bir  44669  snelpwrVD  44869  unipwrVD  44870  sstrALT2VD  44872  elex2VD  44876  elex22VD  44877  eqsbc2VD  44878  zfregs2VD  44879  tpid3gVD  44880  en3lplem1VD  44881  en3lpVD  44883  3ornot23VD  44885  3orbi123VD  44888  sbc3orgVD  44889  exbirVD  44891  3impexpVD  44894  3impexpbicomVD  44895  tratrbVD  44899  al2imVD  44900  syl5impVD  44901  ssralv2VD  44904  ordelordALTVD  44905  sbcim2gVD  44913  trsbcVD  44915  truniALTVD  44916  trintALTVD  44918  undif3VD  44920  sbcssgVD  44921  csbingVD  44922  onfrALTlem3VD  44925  simplbi2comtVD  44926  onfrALTlem2VD  44927  onfrALTVD  44929  csbeq2gVD  44930  csbsngVD  44931  csbxpgVD  44932  csbresgVD  44933  csbrngVD  44934  csbima12gALTVD  44935  csbunigVD  44936  csbfv12gALTVD  44937  con5VD  44938  relopabVD  44939  19.41rgVD  44940  2pm13.193VD  44941  hbimpgVD  44942  hbalgVD  44943  hbexgVD  44944  ax6e2eqVD  44945  ax6e2ndVD  44946  ax6e2ndeqVD  44947  2sb5ndVD  44948  2uasbanhVD  44949  e2ebindVD  44950  sb5ALTVD  44951  vk15.4jVD  44952  notnotrALTVD  44953  con3ALTVD  44954