Theorem pm2.43d 54

Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 57 and pm2.43i 53. (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 23	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 46	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  112  rspct  3566  po2nr  5583  somo  5608  ordelord  6382  tz7.7  6386  funssres  6580  2elresin  6656  dffv2  6976  f1imass  7262  onint  7788  onfununi  8327  smoel  8346  tfrlem11  8374  tfr3  8385  omass  8564  nnmass  8609  sbthlem1  9074  pssnn  9152  php  9190  inf3lem2  9597  cardne  9950  dfac2b  10113  indpi  10891  genpcd  10990  ltexprlem7  11026  addcanpr  11030  reclem4pr  11034  suplem2pr  11037  sup2  12170  nnunb  12499  uzwo  12934  xrub  13337  grpid  19041  lsmcss  21821  uniopn  23033  fclsss1  24158  fclsss2  24159  ltsval2  27796  addonbday  28448  grpoid  30838  spansncvi  31970  pjnormssi  32486  sumdmdlem2  32737  acycgrcycl  35605  meran1  36888  bj-animbi  37117  currysetlem2  37550  bj-elsn0  37765  poimirlem31  38268  heicant  38272  disjimeceqim2  39422  hlhilhillem  42702  sn-sup2  43233  ee223  45313  eel2122old  45396  afv0nbfvbi  47855  fmtnoprmfac1lem  48283