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  3333  po2nr  5077  somo  5098  ordelord  5783  tz7.7  5787  funssres  5968  2elresin  6040  dffv2  6310  f1imass  6561  onint  7037  wfrlem12  7471  wfrlem14  7473  onfununi  7483  smoel  7502  tfrlem11  7529  tfr3  7540  omass  7705  nnmass  7749  sbthlem1  8111  php  8185  inf3lem2  8564  cardne  8829  dfac2  8991  indpi  9767  genpcd  9866  ltexprlem7  9902  addcanpr  9906  reclem4pr  9910  suplem2pr  9913  sup2  11017  nnunb  11326  uzwo  11789  xrub  12180  grpid  17504  lsmcss  20084  uniopn  20750  fclsss1  21873  fclsss2  21874  grpoid  27502  spansncvi  28639  pjnormssi  29155  sumdmdlem2  29406  trpredrec  31862  sltval2  31934  meran1  32535  poimirlem31  33570  heicant  33574  hlhilhillem  37569  ee223  39176  eel2122old  39260  afv0nbfvbi  41552  fmtnoprmfac1lem  41801
  Copyright terms: Public domain W3C validator