Theorem e1a 45703

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45645

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45646

This theorem is used by:  e1bi  45705  e1bir  45706  snelpwrVD  45906  unipwrVD  45907  sstrALT2VD  45909  elex2VD  45913  elex22VD  45914  eqsbc2VD  45915  zfregs2VD  45916  tpid3gVD  45917  en3lplem1VD  45918  en3lpVD  45920  3ornot23VD  45922  3orbi123VD  45925  sbc3orgVD  45926  exbirVD  45928  3impexpVD  45931  3impexpbicomVD  45932  tratrbVD  45936  al2imVD  45937  syl5impVD  45938  ssralv2VD  45941  ordelordALTVD  45942  sbcim2gVD  45950  trsbcVD  45952  truniALTVD  45953  trintALTVD  45955  undif3VD  45957  sbcssgVD  45958  csbingVD  45959  onfrALTlem3VD  45962  simplbi2comtVD  45963  onfrALTlem2VD  45964  onfrALTVD  45966  csbeq2gVD  45967  csbsngVD  45968  csbxpgVD  45969  csbresgVD  45970  csbrngVD  45971  csbima12gALTVD  45972  csbunigVD  45973  csbfv12gALTVD  45974  con5VD  45975  relopabVD  45976  19.41rgVD  45977  2pm13.193VD  45978  hbimpgVD  45979  hbalgVD  45980  hbexgVD  45981  ax6e2eqVD  45982  ax6e2ndVD  45983  ax6e2ndeqVD  45984  2sb5ndVD  45985  2uasbanhVD  45986  e2ebindVD  45987  sb5ALTVD  45988  vk15.4jVD  45989  notnotrALTVD  45990  con3ALTVD  45991