Theorem e1a 44868

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

Syntax hints:   → wi 4  (   wvd1 44810

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 44811

This theorem is referenced by:  e1bi  44870  e1bir  44871  snelpwrVD  45071  unipwrVD  45072  sstrALT2VD  45074  elex2VD  45078  elex22VD  45079  eqsbc2VD  45080  zfregs2VD  45081  tpid3gVD  45082  en3lplem1VD  45083  en3lpVD  45085  3ornot23VD  45087  3orbi123VD  45090  sbc3orgVD  45091  exbirVD  45093  3impexpVD  45096  3impexpbicomVD  45097  tratrbVD  45101  al2imVD  45102  syl5impVD  45103  ssralv2VD  45106  ordelordALTVD  45107  sbcim2gVD  45115  trsbcVD  45117  truniALTVD  45118  trintALTVD  45120  undif3VD  45122  sbcssgVD  45123  csbingVD  45124  onfrALTlem3VD  45127  simplbi2comtVD  45128  onfrALTlem2VD  45129  onfrALTVD  45131  csbeq2gVD  45132  csbsngVD  45133  csbxpgVD  45134  csbresgVD  45135  csbrngVD  45136  csbima12gALTVD  45137  csbunigVD  45138  csbfv12gALTVD  45139  con5VD  45140  relopabVD  45141  19.41rgVD  45142  2pm13.193VD  45143  hbimpgVD  45144  hbalgVD  45145  hbexgVD  45146  ax6e2eqVD  45147  ax6e2ndVD  45148  ax6e2ndeqVD  45149  2sb5ndVD  45150  2uasbanhVD  45151  e2ebindVD  45152  sb5ALTVD  45153  vk15.4jVD  45154  notnotrALTVD  45155  con3ALTVD  45156