Theorem e1a 44652

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

Syntax hints:   → wi 4  (   wvd1 44594

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 44595

This theorem is referenced by:  e1bi  44654  e1bir  44655  snelpwrVD  44856  unipwrVD  44857  sstrALT2VD  44859  elex2VD  44863  elex22VD  44864  eqsbc2VD  44865  zfregs2VD  44866  tpid3gVD  44867  en3lplem1VD  44868  en3lpVD  44870  3ornot23VD  44872  3orbi123VD  44875  sbc3orgVD  44876  exbirVD  44878  3impexpVD  44881  3impexpbicomVD  44882  tratrbVD  44886  al2imVD  44887  syl5impVD  44888  ssralv2VD  44891  ordelordALTVD  44892  sbcim2gVD  44900  trsbcVD  44902  truniALTVD  44903  trintALTVD  44905  undif3VD  44907  sbcssgVD  44908  csbingVD  44909  onfrALTlem3VD  44912  simplbi2comtVD  44913  onfrALTlem2VD  44914  onfrALTVD  44916  csbeq2gVD  44917  csbsngVD  44918  csbxpgVD  44919  csbresgVD  44920  csbrngVD  44921  csbima12gALTVD  44922  csbunigVD  44923  csbfv12gALTVD  44924  con5VD  44925  relopabVD  44926  19.41rgVD  44927  2pm13.193VD  44928  hbimpgVD  44929  hbalgVD  44930  hbexgVD  44931  ax6e2eqVD  44932  ax6e2ndVD  44933  ax6e2ndeqVD  44934  2sb5ndVD  44935  2uasbanhVD  44936  e2ebindVD  44937  sb5ALTVD  44938  vk15.4jVD  44939  notnotrALTVD  44940  con3ALTVD  44941