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  111  rspct  3611  po2nr  5489  somo  5512  ordelord  6215  tz7.7  6219  funssres  6400  2elresin  6470  dffv2  6758  f1imass  7024  onint  7512  wfrlem12  7968  wfrlem14  7970  onfununi  7980  smoel  7999  tfrlem11  8026  tfr3  8037  omass  8208  nnmass  8252  sbthlem1  8629  php  8703  inf3lem2  9094  cardne  9396  dfac2b  9558  indpi  10331  genpcd  10430  ltexprlem7  10466  addcanpr  10470  reclem4pr  10474  suplem2pr  10477  sup2  11599  nnunb  11896  uzwo  12314  xrub  12708  grpid  18141  lsmcss  20838  uniopn  21507  fclsss1  22632  fclsss2  22633  grpoid  28299  spansncvi  29431  pjnormssi  29947  sumdmdlem2  30198  acycgrcycl  32396  trpredrec  33079  sltval2  33165  meran1  33761  bj-animbi  33896  currysetlem2  34261  bj-elsn0  34449  poimirlem31  34925  heicant  34929  hlhilhillem  39098  ee223  40975  eel2122old  41059  afv0nbfvbi  43357  fmtnoprmfac1lem  43733