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  3502  po2nr  5252  somo  5273  ordelord  5965  tz7.7  5969  funssres  6147  2elresin  6216  dffv2  6495  f1imass  6748  onint  7228  wfrlem12  7665  wfrlem14  7667  onfununi  7677  smoel  7696  tfrlem11  7723  tfr3  7734  omass  7900  nnmass  7944  sbthlem1  8312  php  8386  inf3lem2  8776  cardne  9077  dfac2b  9239  dfac2OLD  9241  indpi  10017  genpcd  10116  ltexprlem7  10152  addcanpr  10156  reclem4pr  10160  suplem2pr  10163  sup2  11267  nnunb  11558  uzwo  11973  xrub  12363  grpid  17665  lsmcss  20250  uniopn  20919  fclsss1  22043  fclsss2  22044  grpoid  27709  spansncvi  28845  pjnormssi  29361  sumdmdlem2  29612  trpredrec  32063  sltval2  32135  meran1  32732  poimirlem31  33755  heicant  33759  hlhilhillem  37742  ee223  39358  eel2122old  39442  afv0nbfvbi  41741  fmtnoprmfac1lem  42052
  Copyright terms: Public domain W3C validator