Theorem e1a 40380

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

Syntax hints:   → wi 4  (   wvd1 40322

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 199  df-vd1 40323

This theorem is referenced by:  e1bi  40382  e1bir  40383  snelpwrVD  40584  unipwrVD  40585  sstrALT2VD  40587  elex2VD  40591  elex22VD  40592  eqsbc3rVD  40593  zfregs2VD  40594  tpid3gVD  40595  en3lplem1VD  40596  en3lpVD  40598  3ornot23VD  40600  3orbi123VD  40603  sbc3orgVD  40604  exbirVD  40606  3impexpVD  40609  3impexpbicomVD  40610  tratrbVD  40614  al2imVD  40615  syl5impVD  40616  ssralv2VD  40619  ordelordALTVD  40620  sbcim2gVD  40628  trsbcVD  40630  truniALTVD  40631  trintALTVD  40633  undif3VD  40635  sbcssgVD  40636  csbingVD  40637  onfrALTlem3VD  40640  simplbi2comtVD  40641  onfrALTlem2VD  40642  onfrALTVD  40644  csbeq2gVD  40645  csbsngVD  40646  csbxpgVD  40647  csbresgVD  40648  csbrngVD  40649  csbima12gALTVD  40650  csbunigVD  40651  csbfv12gALTVD  40652  con5VD  40653  relopabVD  40654  19.41rgVD  40655  2pm13.193VD  40656  hbimpgVD  40657  hbalgVD  40658  hbexgVD  40659  ax6e2eqVD  40660  ax6e2ndVD  40661  ax6e2ndeqVD  40662  2sb5ndVD  40663  2uasbanhVD  40664  e2ebindVD  40665  sb5ALTVD  40666  vk15.4jVD  40667  notnotrALTVD  40668  con3ALTVD  40669