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  110  rspct  3442  po2nr  5200  somo  5221  ordelord  5906  tz7.7  5910  funssres  6091  2elresin  6163  dffv2  6434  f1imass  6685  onint  7161  wfrlem12  7596  wfrlem14  7598  onfununi  7608  smoel  7627  tfrlem11  7654  tfr3  7665  omass  7831  nnmass  7875  sbthlem1  8237  php  8311  inf3lem2  8701  cardne  9001  dfac2b  9163  dfac2OLD  9165  indpi  9941  genpcd  10040  ltexprlem7  10076  addcanpr  10080  reclem4pr  10084  suplem2pr  10087  sup2  11191  nnunb  11500  uzwo  11964  xrub  12355  grpid  17678  lsmcss  20258  uniopn  20924  fclsss1  22047  fclsss2  22048  grpoid  27704  spansncvi  28841  pjnormssi  29357  sumdmdlem2  29608  trpredrec  32064  sltval2  32136  meran1  32737  poimirlem31  33771  heicant  33775  hlhilhillem  37772  ee223  39379  eel2122old  39463  afv0nbfvbi  41755  fmtnoprmfac1lem  42004
  Copyright terms: Public domain W3C validator