Theorem e1a 44619

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

Syntax hints:   → wi 4  (   wvd1 44561

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 44562

This theorem is referenced by:  e1bi  44621  e1bir  44622  snelpwrVD  44822  unipwrVD  44823  sstrALT2VD  44825  elex2VD  44829  elex22VD  44830  eqsbc2VD  44831  zfregs2VD  44832  tpid3gVD  44833  en3lplem1VD  44834  en3lpVD  44836  3ornot23VD  44838  3orbi123VD  44841  sbc3orgVD  44842  exbirVD  44844  3impexpVD  44847  3impexpbicomVD  44848  tratrbVD  44852  al2imVD  44853  syl5impVD  44854  ssralv2VD  44857  ordelordALTVD  44858  sbcim2gVD  44866  trsbcVD  44868  truniALTVD  44869  trintALTVD  44871  undif3VD  44873  sbcssgVD  44874  csbingVD  44875  onfrALTlem3VD  44878  simplbi2comtVD  44879  onfrALTlem2VD  44880  onfrALTVD  44882  csbeq2gVD  44883  csbsngVD  44884  csbxpgVD  44885  csbresgVD  44886  csbrngVD  44887  csbima12gALTVD  44888  csbunigVD  44889  csbfv12gALTVD  44890  con5VD  44891  relopabVD  44892  19.41rgVD  44893  2pm13.193VD  44894  hbimpgVD  44895  hbalgVD  44896  hbexgVD  44897  ax6e2eqVD  44898  ax6e2ndVD  44899  ax6e2ndeqVD  44900  2sb5ndVD  44901  2uasbanhVD  44902  e2ebindVD  44903  sb5ALTVD  44904  vk15.4jVD  44905  notnotrALTVD  44906  con3ALTVD  44907