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  5554  somo  5579  ordelord  6347  tz7.7  6351  funssres  6544  2elresin  6621  dffv2  6937  f1imass  7221  onint  7746  onfununi  8283  smoel  8302  tfrlem11  8329  tfr3  8340  omass  8517  nnmass  8562  sbthlem1  9027  pssnn  9105  php  9143  inf3lem2  9552  cardne  9891  dfac2b  10055  indpi  10832  genpcd  10931  ltexprlem7  10967  addcanpr  10971  reclem4pr  10975  suplem2pr  10978  sup2  12114  nnunb  12435  uzwo  12863  xrub  13266  grpid  18953  lsmcss  21674  uniopn  22864  fclsss1  23989  fclsss2  23990  ltsval2  27622  addonbday  28273  grpoid  30593  spansncvi  31725  pjnormssi  32241  sumdmdlem2  32492  acycgrcycl  35331  meran1  36595  bj-animbi  36825  currysetlem2  37257  bj-elsn0  37471  poimirlem31  37974  heicant  37978  disjimeceqim2  39128  hlhilhillem  42408  sn-sup2  42938  ee223  45063  eel2122old  45146  afv0nbfvbi  47601  fmtnoprmfac1lem  48029