MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.43d Structured version   Visualization version   GIF version

Theorem pm2.43d 53
Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 56 and pm2.43i 52. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43d.1 (𝜑 → (𝜓 → (𝜓𝜒)))
Assertion
Ref Expression
pm2.43d (𝜑 → (𝜓𝜒))

Proof of Theorem pm2.43d
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
2 pm2.43d.1 . 2 (𝜑 → (𝜓 → (𝜓𝜒)))
31, 2mpdi 45 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  loolin  111  rspct  3613  po2nr  5486  somo  5509  ordelord  6212  tz7.7  6216  funssres  6397  2elresin  6467  dffv2  6755  f1imass  7018  onint  7503  wfrlem12  7962  wfrlem14  7964  onfununi  7974  smoel  7993  tfrlem11  8020  tfr3  8031  omass  8201  nnmass  8245  sbthlem1  8621  php  8695  inf3lem2  9086  cardne  9388  dfac2b  9550  indpi  10323  genpcd  10422  ltexprlem7  10458  addcanpr  10462  reclem4pr  10466  suplem2pr  10469  sup2  11591  nnunb  11887  uzwo  12305  xrub  12700  grpid  18084  lsmcss  20771  uniopn  21440  fclsss1  22565  fclsss2  22566  grpoid  28230  spansncvi  29362  pjnormssi  29878  sumdmdlem2  30129  acycgrcycl  32297  trpredrec  32980  sltval2  33066  meran1  33662  bj-animbi  33797  currysetlem2  34162  bj-elsn0  34345  poimirlem31  34809  heicant  34813  hlhilhillem  38982  ee223  40852  eel2122old  40936  afv0nbfvbi  43235  fmtnoprmfac1lem  43577
  Copyright terms: Public domain W3C validator