HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem pm2.43d 65
Description: Deduction absorbing redundant antecedent. (The proof was shortened by O'Cat, 3-Feb-06.)
Hypothesis
Ref Expression
pm2.43d.1 |- (ph -> (ps -> (ps -> ch)))
Assertion
Ref Expression
pm2.43d |- (ph -> (ps -> ch))
Proof of Theorem pm2.43d
StepHypRef Expression
1 idd 61 . 2 |- (ph -> (ps -> ps))
2 pm2.43d.1 . 2 |- (ph -> (ps -> (ps -> ch)))
31, 2mpdd 46 1 |- (ph -> (ps -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  loolin 72  3anidm23 881  po2nr 2838  wereu 2935  ordelord 2960  tz7.7 2963  ordtr2 2992  onint 2996  ordsucelsuc 3063  funssres 3538  2elresin 3584  funfvop 3788  funiunfv 3851  isofrlem 3886  tfrlem11 3906  tfr3 3911  omass 4195  sbthlem1 4427  php 4493  inf3lem2 4586  r1ord 4627  aceq6b 4714  indpi 5006  genpcd 5081  ltaddpr 5112  ltexprlem7 5120  addcanpr 5124  prlem936 5127  reclem4pr 5131  suplem2pr 5134  suppsr2 5195  sup2 5998  nnunb 6017  xrub 6027  uzwo4OLD 6158  ser1add2 6275  uzwo 6387  uzwoOLD 6388  climcmplem 7073  georeclim 7175  infcda 7510  uniopnt 7540  metge0 7760  grpid 7999  psdmrn 8574  psref 8575  spansncv 9514  pjnormss 10007  sumdmdlem2 10253  hmeomap 10405  hmeocna 10406  hmeocnb 10407  hmeogrp 10425  fillsb 10435  fmamo 10594  vidfunid 10595  iddvvidd 10596  idcvvidc 10597
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain