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  3551  po2nr  5553  somo  5578  ordelord  6346  tz7.7  6350  funssres  6543  2elresin  6620  dffv2  6936  f1imass  7219  onint  7744  onfununi  8281  smoel  8300  tfrlem11  8327  tfr3  8338  omass  8515  nnmass  8560  sbthlem1  9025  pssnn  9103  php  9141  inf3lem2  9550  cardne  9889  dfac2b  10053  indpi  10830  genpcd  10929  ltexprlem7  10965  addcanpr  10969  reclem4pr  10973  suplem2pr  10976  sup2  12112  nnunb  12433  uzwo  12861  xrub  13264  grpid  18951  lsmcss  21672  uniopn  22862  fclsss1  23987  fclsss2  23988  ltsval2  27620  addonbday  28271  grpoid  30591  spansncvi  31723  pjnormssi  32239  sumdmdlem2  32490  acycgrcycl  35329  meran1  36593  bj-animbi  36823  currysetlem2  37255  bj-elsn0  37469  poimirlem31  37972  heicant  37976  disjimeceqim2  39126  hlhilhillem  42406  sn-sup2  42936  ee223  45061  eel2122old  45144  afv0nbfvbi  47593  fmtnoprmfac1lem  48021