Theorem pm2.43d 65

Description: Deduction absorbing redundant antecedent. (The proof was shortened by O'Cat, 3-Feb-2006.)

Hypothesis

Ref	Expression
pm2.43d.1	|- (ph -> (ps -> (ps -> ch)))

Assertion

Ref	Expression
pm2.43d	|- (ph -> (ps -> ch))

Proof of Theorem pm2.43d

Step	Hyp	Ref	Expression
1		idd 61	. 2 |- (ph -> (ps -> ps))
2		pm2.43d.1	. 2 |- (ph -> (ps -> (ps -> ch)))
3	1, 2	mpdd 46	1 |- (ph -> (ps -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  loolin 72  3anidm23 884  po2nr 2847  wereu 2945  ordelord 2970  tz7.7 2973  ordtr2 3002  onint 3006  ordsucelsuc 3073  funssres 3552  2elresin 3598  funfvop 3803  funiunfv 3866  isofrlem 3901  tfrlem11 3921  tfr3 3926  omass 4211  sbthlem1 4447  php 4513  inf3lem2 4614  r1ord 4655  aceq6b 4742  indpi 5034  genpcd 5109  ltaddpr 5140  ltexprlem7 5148  addcanpr 5152  prlem936 5155  reclem4pr 5159  suplem2pr 5162  suppsr2 5223  sup2 6051  nnunb 6070  xrub 6080  uzwo4OLD 6210  ser1add2 6338  uzwo 6455  uzwoOLD 6456  climcmplem 7137  georeclim 7240  infcda 7567  uniopnt 7598  metge0 7819  grpid 8065  psdmrn 8648  psref 8649  spansncv 9597  pjnormss 10096  sumdmdlem2 10346  hmeomap 10518  hmeocna 10519  hmeocnb 10520  hmeogrp 10538  fillsb 10560  fmamo 10756  vidfunid 10757  iddvvidd 10758  idcvvidc 10759

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain