Theorem e1a 39446

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

Syntax hints:   → wi 4  (   wvd1 39379

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 198  df-vd1 39380

This theorem is referenced by:  e1bi  39448  e1bir  39449  snelpwrVD  39651  unipwrVD  39652  sstrALT2VD  39654  elex2VD  39658  elex22VD  39659  eqsbc3rVD  39660  zfregs2VD  39661  tpid3gVD  39662  en3lplem1VD  39663  en3lpVD  39665  3ornot23VD  39667  3orbi123VD  39670  sbc3orgVD  39671  exbirVD  39673  3impexpVD  39676  3impexpbicomVD  39677  tratrbVD  39681  al2imVD  39682  syl5impVD  39683  ssralv2VD  39686  ordelordALTVD  39687  sbcim2gVD  39695  trsbcVD  39697  truniALTVD  39698  trintALTVD  39700  undif3VD  39702  sbcssgVD  39703  csbingVD  39704  onfrALTlem3VD  39707  simplbi2comtVD  39708  onfrALTlem2VD  39709  onfrALTVD  39711  csbeq2gVD  39712  csbsngVD  39713  csbxpgVD  39714  csbresgVD  39715  csbrngVD  39716  csbima12gALTVD  39717  csbunigVD  39718  csbfv12gALTVD  39719  con5VD  39720  relopabVD  39721  19.41rgVD  39722  2pm13.193VD  39723  hbimpgVD  39724  hbalgVD  39725  hbexgVD  39726  ax6e2eqVD  39727  ax6e2ndVD  39728  ax6e2ndeqVD  39729  2sb5ndVD  39730  2uasbanhVD  39731  e2ebindVD  39732  sb5ALTVD  39733  vk15.4jVD  39734  notnotrALTVD  39735  con3ALTVD  39736