Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e1a Structured version   Visualization version   GIF version

Theorem e1a 43321
Description: A Virtual deduction elimination rule. syl 17 is e1a 43321 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
StepHypRef Expression
1 e1a.1 . . . 4 (   𝜑   ▶   𝜓   )
21in1 43265 . . 3 (𝜑𝜓)
3 e1a.2 . . 3 (𝜓𝜒)
42, 3syl 17 . 2 (𝜑𝜒)
54dfvd1ir 43267 1 (   𝜑   ▶   𝜒   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 43263
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 206  df-vd1 43264
This theorem is referenced by:  e1bi  43323  e1bir  43324  snelpwrVD  43525  unipwrVD  43526  sstrALT2VD  43528  elex2VD  43532  elex22VD  43533  eqsbc2VD  43534  zfregs2VD  43535  tpid3gVD  43536  en3lplem1VD  43537  en3lpVD  43539  3ornot23VD  43541  3orbi123VD  43544  sbc3orgVD  43545  exbirVD  43547  3impexpVD  43550  3impexpbicomVD  43551  tratrbVD  43555  al2imVD  43556  syl5impVD  43557  ssralv2VD  43560  ordelordALTVD  43561  sbcim2gVD  43569  trsbcVD  43571  truniALTVD  43572  trintALTVD  43574  undif3VD  43576  sbcssgVD  43577  csbingVD  43578  onfrALTlem3VD  43581  simplbi2comtVD  43582  onfrALTlem2VD  43583  onfrALTVD  43585  csbeq2gVD  43586  csbsngVD  43587  csbxpgVD  43588  csbresgVD  43589  csbrngVD  43590  csbima12gALTVD  43591  csbunigVD  43592  csbfv12gALTVD  43593  con5VD  43594  relopabVD  43595  19.41rgVD  43596  2pm13.193VD  43597  hbimpgVD  43598  hbalgVD  43599  hbexgVD  43600  ax6e2eqVD  43601  ax6e2ndVD  43602  ax6e2ndeqVD  43603  2sb5ndVD  43604  2uasbanhVD  43605  e2ebindVD  43606  sb5ALTVD  43607  vk15.4jVD  43608  notnotrALTVD  43609  con3ALTVD  43610
  Copyright terms: Public domain W3C validator