Theorem e1a 45319

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

Syntax hints:   → wi 4  (   wvd1 45261

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 210  df-vd1 45262

This theorem is referenced by:  e1bi  45321  e1bir  45322  snelpwrVD  45522  unipwrVD  45523  sstrALT2VD  45525  elex2VD  45529  elex22VD  45530  eqsbc2VD  45531  zfregs2VD  45532  tpid3gVD  45533  en3lplem1VD  45534  en3lpVD  45536  3ornot23VD  45538  3orbi123VD  45541  sbc3orgVD  45542  exbirVD  45544  3impexpVD  45547  3impexpbicomVD  45548  tratrbVD  45552  al2imVD  45553  syl5impVD  45554  ssralv2VD  45557  ordelordALTVD  45558  sbcim2gVD  45566  trsbcVD  45568  truniALTVD  45569  trintALTVD  45571  undif3VD  45573  sbcssgVD  45574  csbingVD  45575  onfrALTlem3VD  45578  simplbi2comtVD  45579  onfrALTlem2VD  45580  onfrALTVD  45582  csbeq2gVD  45583  csbsngVD  45584  csbxpgVD  45585  csbresgVD  45586  csbrngVD  45587  csbima12gALTVD  45588  csbunigVD  45589  csbfv12gALTVD  45590  con5VD  45591  relopabVD  45592  19.41rgVD  45593  2pm13.193VD  45594  hbimpgVD  45595  hbalgVD  45596  hbexgVD  45597  ax6e2eqVD  45598  ax6e2ndVD  45599  ax6e2ndeqVD  45600  2sb5ndVD  45601  2uasbanhVD  45602  e2ebindVD  45603  sb5ALTVD  45604  vk15.4jVD  45605  notnotrALTVD  45606  con3ALTVD  45607