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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 45	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  3292  po2nr  5018  somo  5039  ordelord  5714  tz7.7  5718  funssres  5898  2elresin  5970  dffv2  6238  f1imass  6486  onint  6957  wfrlem12  7386  wfrlem14  7388  onfununi  7398  smoel  7417  tfrlem11  7444  tfr3  7455  omass  7620  nnmass  7664  sbthlem1  8030  php  8104  inf3lem2  8486  cardne  8751  dfac2  8913  indpi  9689  genpcd  9788  ltexprlem7  9824  addcanpr  9828  reclem4pr  9832  suplem2pr  9835  sup2  10939  nnunb  11248  uzwo  11711  xrub  12101  grpid  17397  lsmcss  19976  uniopn  20642  fclsss1  21766  fclsss2  21767  frgr2wwlk1  27086  grpoid  27262  spansncvi  28399  pjnormssi  28915  sumdmdlem2  29166  trpredrec  31492  frrlem11  31546  sltval2  31563  nobndup  31616  nobnddown  31617  meran1  32105  poimirlem31  33111  heicant  33115  hlhilhillem  36771  ee223  38380  eel2122old  38464  afv0nbfvbi  40565