Theorem e1a 45072

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

Syntax hints:   → wi 4  (   wvd1 45014

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 45015

This theorem is referenced by:  e1bi  45074  e1bir  45075  snelpwrVD  45275  unipwrVD  45276  sstrALT2VD  45278  elex2VD  45282  elex22VD  45283  eqsbc2VD  45284  zfregs2VD  45285  tpid3gVD  45286  en3lplem1VD  45287  en3lpVD  45289  3ornot23VD  45291  3orbi123VD  45294  sbc3orgVD  45295  exbirVD  45297  3impexpVD  45300  3impexpbicomVD  45301  tratrbVD  45305  al2imVD  45306  syl5impVD  45307  ssralv2VD  45310  ordelordALTVD  45311  sbcim2gVD  45319  trsbcVD  45321  truniALTVD  45322  trintALTVD  45324  undif3VD  45326  sbcssgVD  45327  csbingVD  45328  onfrALTlem3VD  45331  simplbi2comtVD  45332  onfrALTlem2VD  45333  onfrALTVD  45335  csbeq2gVD  45336  csbsngVD  45337  csbxpgVD  45338  csbresgVD  45339  csbrngVD  45340  csbima12gALTVD  45341  csbunigVD  45342  csbfv12gALTVD  45343  con5VD  45344  relopabVD  45345  19.41rgVD  45346  2pm13.193VD  45347  hbimpgVD  45348  hbalgVD  45349  hbexgVD  45350  ax6e2eqVD  45351  ax6e2ndVD  45352  ax6e2ndeqVD  45353  2sb5ndVD  45354  2uasbanhVD  45355  e2ebindVD  45356  sb5ALTVD  45357  vk15.4jVD  45358  notnotrALTVD  45359  con3ALTVD  45360