Theorem e1a 45078

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

Syntax hints:   → wi 4  (   wvd1 45020

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 208  df-vd1 45021

This theorem is referenced by:  e1bi  45080  e1bir  45081  snelpwrVD  45281  unipwrVD  45282  sstrALT2VD  45284  elex2VD  45288  elex22VD  45289  eqsbc2VD  45290  zfregs2VD  45291  tpid3gVD  45292  en3lplem1VD  45293  en3lpVD  45295  3ornot23VD  45297  3orbi123VD  45300  sbc3orgVD  45301  exbirVD  45303  3impexpVD  45306  3impexpbicomVD  45307  tratrbVD  45311  al2imVD  45312  syl5impVD  45313  ssralv2VD  45316  ordelordALTVD  45317  sbcim2gVD  45325  trsbcVD  45327  truniALTVD  45328  trintALTVD  45330  undif3VD  45332  sbcssgVD  45333  csbingVD  45334  onfrALTlem3VD  45337  simplbi2comtVD  45338  onfrALTlem2VD  45339  onfrALTVD  45341  csbeq2gVD  45342  csbsngVD  45343  csbxpgVD  45344  csbresgVD  45345  csbrngVD  45346  csbima12gALTVD  45347  csbunigVD  45348  csbfv12gALTVD  45349  con5VD  45350  relopabVD  45351  19.41rgVD  45352  2pm13.193VD  45353  hbimpgVD  45354  hbalgVD  45355  hbexgVD  45356  ax6e2eqVD  45357  ax6e2ndVD  45358  ax6e2ndeqVD  45359  2sb5ndVD  45360  2uasbanhVD  45361  e2ebindVD  45362  sb5ALTVD  45363  vk15.4jVD  45364  notnotrALTVD  45365  con3ALTVD  45366