Theorem e1a 44617

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

Syntax hints:   → wi 4  (   wvd1 44559

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 44560

This theorem is referenced by:  e1bi  44619  e1bir  44620  snelpwrVD  44820  unipwrVD  44821  sstrALT2VD  44823  elex2VD  44827  elex22VD  44828  eqsbc2VD  44829  zfregs2VD  44830  tpid3gVD  44831  en3lplem1VD  44832  en3lpVD  44834  3ornot23VD  44836  3orbi123VD  44839  sbc3orgVD  44840  exbirVD  44842  3impexpVD  44845  3impexpbicomVD  44846  tratrbVD  44850  al2imVD  44851  syl5impVD  44852  ssralv2VD  44855  ordelordALTVD  44856  sbcim2gVD  44864  trsbcVD  44866  truniALTVD  44867  trintALTVD  44869  undif3VD  44871  sbcssgVD  44872  csbingVD  44873  onfrALTlem3VD  44876  simplbi2comtVD  44877  onfrALTlem2VD  44878  onfrALTVD  44880  csbeq2gVD  44881  csbsngVD  44882  csbxpgVD  44883  csbresgVD  44884  csbrngVD  44885  csbima12gALTVD  44886  csbunigVD  44887  csbfv12gALTVD  44888  con5VD  44889  relopabVD  44890  19.41rgVD  44891  2pm13.193VD  44892  hbimpgVD  44893  hbalgVD  44894  hbexgVD  44895  ax6e2eqVD  44896  ax6e2ndVD  44897  ax6e2ndeqVD  44898  2sb5ndVD  44899  2uasbanhVD  44900  e2ebindVD  44901  sb5ALTVD  44902  vk15.4jVD  44903  notnotrALTVD  44904  con3ALTVD  44905