Theorem e1a 43321

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

Syntax hints:   → wi 4  (   wvd1 43263

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 43264

This theorem is referenced by:  e1bi  43323  e1bir  43324  snelpwrVD  43525  unipwrVD  43526  sstrALT2VD  43528  elex2VD  43532  elex22VD  43533  eqsbc2VD  43534  zfregs2VD  43535  tpid3gVD  43536  en3lplem1VD  43537  en3lpVD  43539  3ornot23VD  43541  3orbi123VD  43544  sbc3orgVD  43545  exbirVD  43547  3impexpVD  43550  3impexpbicomVD  43551  tratrbVD  43555  al2imVD  43556  syl5impVD  43557  ssralv2VD  43560  ordelordALTVD  43561  sbcim2gVD  43569  trsbcVD  43571  truniALTVD  43572  trintALTVD  43574  undif3VD  43576  sbcssgVD  43577  csbingVD  43578  onfrALTlem3VD  43581  simplbi2comtVD  43582  onfrALTlem2VD  43583  onfrALTVD  43585  csbeq2gVD  43586  csbsngVD  43587  csbxpgVD  43588  csbresgVD  43589  csbrngVD  43590  csbima12gALTVD  43591  csbunigVD  43592  csbfv12gALTVD  43593  con5VD  43594  relopabVD  43595  19.41rgVD  43596  2pm13.193VD  43597  hbimpgVD  43598  hbalgVD  43599  hbexgVD  43600  ax6e2eqVD  43601  ax6e2ndVD  43602  ax6e2ndeqVD  43603  2sb5ndVD  43604  2uasbanhVD  43605  e2ebindVD  43606  sb5ALTVD  43607  vk15.4jVD  43608  notnotrALTVD  43609  con3ALTVD  43610