Theorem e1a 39169

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

Syntax hints:   → wi 4  (   wvd1 39102

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 197  df-vd1 39103

This theorem is referenced by:  e1bi  39171  e1bir  39172  snelpwrVD  39380  unipwrVD  39381  sstrALT2VD  39383  elex2VD  39387  elex22VD  39388  eqsbc3rVD  39389  zfregs2VD  39390  tpid3gVD  39391  en3lplem1VD  39392  en3lpVD  39394  3ornot23VD  39396  3orbi123VD  39399  sbc3orgVD  39400  exbirVD  39402  3impexpVD  39405  3impexpbicomVD  39406  sbcoreleleqVD  39409  tratrbVD  39411  al2imVD  39412  syl5impVD  39413  ssralv2VD  39416  ordelordALTVD  39417  sbcim2gVD  39425  trsbcVD  39427  truniALTVD  39428  trintALTVD  39430  undif3VD  39432  sbcssgVD  39433  csbingVD  39434  onfrALTlem3VD  39437  simplbi2comtVD  39438  onfrALTlem2VD  39439  onfrALTVD  39441  csbeq2gVD  39442  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  con5VD  39450  relopabVD  39451  19.41rgVD  39452  2pm13.193VD  39453  hbimpgVD  39454  hbalgVD  39455  hbexgVD  39456  ax6e2eqVD  39457  ax6e2ndVD  39458  ax6e2ndeqVD  39459  2sb5ndVD  39460  2uasbanhVD  39461  e2ebindVD  39462  sb5ALTVD  39463  vk15.4jVD  39464  notnotrALTVD  39465  con3ALTVD  39466