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

Theorem e1a 41348
 Description: A Virtual deduction elimination rule. syl 17 is e1a 41348 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 41292 . . 3 (𝜑𝜓)
3 e1a.2 . . 3 (𝜓𝜒)
42, 3syl 17 . 2 (𝜑𝜒)
54dfvd1ir 41294 1 (   𝜑   ▶   𝜒   )
 Colors of variables: wff setvar class Syntax hints:   → wi 4  (   wvd1 41290 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 210  df-vd1 41291 This theorem is referenced by:  e1bi  41350  e1bir  41351  snelpwrVD  41552  unipwrVD  41553  sstrALT2VD  41555  elex2VD  41559  elex22VD  41560  eqsbc3rVD  41561  zfregs2VD  41562  tpid3gVD  41563  en3lplem1VD  41564  en3lpVD  41566  3ornot23VD  41568  3orbi123VD  41571  sbc3orgVD  41572  exbirVD  41574  3impexpVD  41577  3impexpbicomVD  41578  tratrbVD  41582  al2imVD  41583  syl5impVD  41584  ssralv2VD  41587  ordelordALTVD  41588  sbcim2gVD  41596  trsbcVD  41598  truniALTVD  41599  trintALTVD  41601  undif3VD  41603  sbcssgVD  41604  csbingVD  41605  onfrALTlem3VD  41608  simplbi2comtVD  41609  onfrALTlem2VD  41610  onfrALTVD  41612  csbeq2gVD  41613  csbsngVD  41614  csbxpgVD  41615  csbresgVD  41616  csbrngVD  41617  csbima12gALTVD  41618  csbunigVD  41619  csbfv12gALTVD  41620  con5VD  41621  relopabVD  41622  19.41rgVD  41623  2pm13.193VD  41624  hbimpgVD  41625  hbalgVD  41626  hbexgVD  41627  ax6e2eqVD  41628  ax6e2ndVD  41629  ax6e2ndeqVD  41630  2sb5ndVD  41631  2uasbanhVD  41632  e2ebindVD  41633  sb5ALTVD  41634  vk15.4jVD  41635  notnotrALTVD  41636  con3ALTVD  41637
 Copyright terms: Public domain W3C validator