Theorem e1a 45054

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

Syntax hints:   → wi 4  (   wvd1 44996

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 44997

This theorem is referenced by:  e1bi  45056  e1bir  45057  snelpwrVD  45257  unipwrVD  45258  sstrALT2VD  45260  elex2VD  45264  elex22VD  45265  eqsbc2VD  45266  zfregs2VD  45267  tpid3gVD  45268  en3lplem1VD  45269  en3lpVD  45271  3ornot23VD  45273  3orbi123VD  45276  sbc3orgVD  45277  exbirVD  45279  3impexpVD  45282  3impexpbicomVD  45283  tratrbVD  45287  al2imVD  45288  syl5impVD  45289  ssralv2VD  45292  ordelordALTVD  45293  sbcim2gVD  45301  trsbcVD  45303  truniALTVD  45304  trintALTVD  45306  undif3VD  45308  sbcssgVD  45309  csbingVD  45310  onfrALTlem3VD  45313  simplbi2comtVD  45314  onfrALTlem2VD  45315  onfrALTVD  45317  csbeq2gVD  45318  csbsngVD  45319  csbxpgVD  45320  csbresgVD  45321  csbrngVD  45322  csbima12gALTVD  45323  csbunigVD  45324  csbfv12gALTVD  45325  con5VD  45326  relopabVD  45327  19.41rgVD  45328  2pm13.193VD  45329  hbimpgVD  45330  hbalgVD  45331  hbexgVD  45332  ax6e2eqVD  45333  ax6e2ndVD  45334  ax6e2ndeqVD  45335  2sb5ndVD  45336  2uasbanhVD  45337  e2ebindVD  45338  sb5ALTVD  45339  vk15.4jVD  45340  notnotrALTVD  45341  con3ALTVD  45342