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  5544  somo  5569  ordelord  6337  tz7.7  6341  funssres  6534  2elresin  6611  dffv2  6927  f1imass  7210  onint  7735  onfununi  8272  smoel  8291  tfrlem11  8318  tfr3  8329  omass  8506  nnmass  8551  sbthlem1  9016  pssnn  9094  php  9132  inf3lem2  9539  cardne  9878  dfac2b  10042  indpi  10819  genpcd  10918  ltexprlem7  10954  addcanpr  10958  reclem4pr  10962  suplem2pr  10965  sup2  12101  nnunb  12422  uzwo  12850  xrub  13253  grpid  18940  lsmcss  21680  uniopn  22871  fclsss1  23996  fclsss2  23997  ltsval2  27639  addonbday  28290  grpoid  30611  spansncvi  31743  pjnormssi  32259  sumdmdlem2  32510  acycgrcycl  35350  meran1  36614  bj-animbi  36836  currysetlem2  37268  bj-elsn0  37482  poimirlem31  37983  heicant  37987  disjimeceqim2  39137  hlhilhillem  42417  sn-sup2  42947  ee223  45076  eel2122old  45159  afv0nbfvbi  47596  fmtnoprmfac1lem  48024