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 886  po2nr 2853  wereu 2951  ordelord 2976  tz7.7 2979  ordtr2 3008  onint 3012  ordsucelsuc 3079  funssres 3558  2elresin 3604  funfvop 3809  funiunfv 3872  isofrlem 3907  tfrlem11 3927  tfr3 3932  omass 4217  sbthlem1 4453  php 4519  inf3lem2 4623  r1ord 4665  aceq6b 4752  indpi 5046  genpcd 5121  ltaddpr 5152  ltexprlem7 5160  addcanpr 5164  prlem936 5167  reclem4pr 5171  suplem2pr 5174  suppsr2 5235  sup2 6053  nnunb 6072  xrub 6082  uzwo4OLD 6212  ser1add2 6339  uzwo 6456  uzwoOLD 6457  climcmplem 7137  georeclim 7240  infcda 7568  uniopnt 7599  metge0 7816  grpid 8061  psdmrn 8644  psref 8645  spansncv 9592  pjnormss 10091  sumdmdlem2 10341  hmeomap 10504  hmeocna 10505  hmeocnb 10506  hmeogrp 10524  fillsb 10546  fmamo 10727  vidfunid 10728  iddvvidd 10729  idcvvidc 10730

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

Copyright terms: Public domain