Theorem e1a 44604

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

Syntax hints:   → wi 4  (   wvd1 44546

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 44547

This theorem is referenced by:  e1bi  44606  e1bir  44607  snelpwrVD  44807  unipwrVD  44808  sstrALT2VD  44810  elex2VD  44814  elex22VD  44815  eqsbc2VD  44816  zfregs2VD  44817  tpid3gVD  44818  en3lplem1VD  44819  en3lpVD  44821  3ornot23VD  44823  3orbi123VD  44826  sbc3orgVD  44827  exbirVD  44829  3impexpVD  44832  3impexpbicomVD  44833  tratrbVD  44837  al2imVD  44838  syl5impVD  44839  ssralv2VD  44842  ordelordALTVD  44843  sbcim2gVD  44851  trsbcVD  44853  truniALTVD  44854  trintALTVD  44856  undif3VD  44858  sbcssgVD  44859  csbingVD  44860  onfrALTlem3VD  44863  simplbi2comtVD  44864  onfrALTlem2VD  44865  onfrALTVD  44867  csbeq2gVD  44868  csbsngVD  44869  csbxpgVD  44870  csbresgVD  44871  csbrngVD  44872  csbima12gALTVD  44873  csbunigVD  44874  csbfv12gALTVD  44875  con5VD  44876  relopabVD  44877  19.41rgVD  44878  2pm13.193VD  44879  hbimpgVD  44880  hbalgVD  44881  hbexgVD  44882  ax6e2eqVD  44883  ax6e2ndVD  44884  ax6e2ndeqVD  44885  2sb5ndVD  44886  2uasbanhVD  44887  e2ebindVD  44888  sb5ALTVD  44889  vk15.4jVD  44890  notnotrALTVD  44891  con3ALTVD  44892