Theorem e1a 43373

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

Syntax hints:   → wi 4  (   wvd1 43315

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 206  df-vd1 43316

This theorem is referenced by:  e1bi  43375  e1bir  43376  snelpwrVD  43577  unipwrVD  43578  sstrALT2VD  43580  elex2VD  43584  elex22VD  43585  eqsbc2VD  43586  zfregs2VD  43587  tpid3gVD  43588  en3lplem1VD  43589  en3lpVD  43591  3ornot23VD  43593  3orbi123VD  43596  sbc3orgVD  43597  exbirVD  43599  3impexpVD  43602  3impexpbicomVD  43603  tratrbVD  43607  al2imVD  43608  syl5impVD  43609  ssralv2VD  43612  ordelordALTVD  43613  sbcim2gVD  43621  trsbcVD  43623  truniALTVD  43624  trintALTVD  43626  undif3VD  43628  sbcssgVD  43629  csbingVD  43630  onfrALTlem3VD  43633  simplbi2comtVD  43634  onfrALTlem2VD  43635  onfrALTVD  43637  csbeq2gVD  43638  csbsngVD  43639  csbxpgVD  43640  csbresgVD  43641  csbrngVD  43642  csbima12gALTVD  43643  csbunigVD  43644  csbfv12gALTVD  43645  con5VD  43646  relopabVD  43647  19.41rgVD  43648  2pm13.193VD  43649  hbimpgVD  43650  hbalgVD  43651  hbexgVD  43652  ax6e2eqVD  43653  ax6e2ndVD  43654  ax6e2ndeqVD  43655  2sb5ndVD  43656  2uasbanhVD  43657  e2ebindVD  43658  sb5ALTVD  43659  vk15.4jVD  43660  notnotrALTVD  43661  con3ALTVD  43662