Theorem e1a 44598

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

Syntax hints:   → wi 4  (   wvd1 44540

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 44541

This theorem is referenced by:  e1bi  44600  e1bir  44601  snelpwrVD  44802  unipwrVD  44803  sstrALT2VD  44805  elex2VD  44809  elex22VD  44810  eqsbc2VD  44811  zfregs2VD  44812  tpid3gVD  44813  en3lplem1VD  44814  en3lpVD  44816  3ornot23VD  44818  3orbi123VD  44821  sbc3orgVD  44822  exbirVD  44824  3impexpVD  44827  3impexpbicomVD  44828  tratrbVD  44832  al2imVD  44833  syl5impVD  44834  ssralv2VD  44837  ordelordALTVD  44838  sbcim2gVD  44846  trsbcVD  44848  truniALTVD  44849  trintALTVD  44851  undif3VD  44853  sbcssgVD  44854  csbingVD  44855  onfrALTlem3VD  44858  simplbi2comtVD  44859  onfrALTlem2VD  44860  onfrALTVD  44862  csbeq2gVD  44863  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  con5VD  44871  relopabVD  44872  19.41rgVD  44873  2pm13.193VD  44874  hbimpgVD  44875  hbalgVD  44876  hbexgVD  44877  ax6e2eqVD  44878  ax6e2ndVD  44879  ax6e2ndeqVD  44880  2sb5ndVD  44881  2uasbanhVD  44882  e2ebindVD  44883  sb5ALTVD  44884  vk15.4jVD  44885  notnotrALTVD  44886  con3ALTVD  44887