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  3609  po2nr  5482  somo  5505  ordelord  6208  tz7.7  6212  funssres  6393  2elresin  6463  dffv2  6751  f1imass  7016  onint  7504  wfrlem12  7960  wfrlem14  7962  onfununi  7972  smoel  7991  tfrlem11  8018  tfr3  8029  omass  8200  nnmass  8244  sbthlem1  8621  php  8695  inf3lem2  9086  cardne  9388  dfac2b  9550  indpi  10323  genpcd  10422  ltexprlem7  10458  addcanpr  10462  reclem4pr  10466  suplem2pr  10469  sup2  11591  nnunb  11887  uzwo  12305  xrub  12699  grpid  18133  lsmcss  20830  uniopn  21499  fclsss1  22624  fclsss2  22625  grpoid  28291  spansncvi  29423  pjnormssi  29939  sumdmdlem2  30190  acycgrcycl  32389  trpredrec  33072  sltval2  33158  meran1  33754  bj-animbi  33889  currysetlem2  34254  bj-elsn0  34441  poimirlem31  34917  heicant  34921  hlhilhillem  39090  ee223  40961  eel2122old  41045  afv0nbfvbi  43343  fmtnoprmfac1lem  43719