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	|- ( ph -> ( ps -> ( ps -> ch ) ) )

Assertion

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

Proof of Theorem pm2.43d

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ps -> ps )
2		pm2.43d.1	. 2 |- ( ph -> ( ps -> ( ps -> ch ) ) )
3	1, 2	mpdi 45	1 |- ( ph -> ( ps -> ch ) )

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  3302  po2nr  5048  somo  5069  ordelord  5745  tz7.7  5749  funssres  5930  2elresin  6002  dffv2  6271  f1imass  6521  onint  6995  wfrlem12  7426  wfrlem14  7428  onfununi  7438  smoel  7457  tfrlem11  7484  tfr3  7495  omass  7660  nnmass  7704  sbthlem1  8070  php  8144  inf3lem2  8526  cardne  8791  dfac2  8953  indpi  9729  genpcd  9828  ltexprlem7  9864  addcanpr  9868  reclem4pr  9872  suplem2pr  9875  sup2  10979  nnunb  11288  uzwo  11751  xrub  12142  grpid  17457  lsmcss  20036  uniopn  20702  fclsss1  21826  fclsss2  21827  grpoid  27374  spansncvi  28511  pjnormssi  29027  sumdmdlem2  29278  trpredrec  31738  frrlem11  31792  sltval2  31809  meran1  32410  poimirlem31  33440  heicant  33444  hlhilhillem  37252  ee223  38859  eel2122old  38943  afv0nbfvbi  41231