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 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  loolin  112  rspct  3562  po2nr  5569  somo  5594  ordelord  6373  tz7.7  6377  funssres  6572  2elresin  6648  dffv2  6968  f1imass  7256  onint  7787  onfununi  8327  smoel  8346  tfrlem11  8374  tfr3  8385  omass  8566  nnmass  8611  sbthlem1  9084  pssnn  9162  php  9200  inf3lem2  9608  cardne  10018  dfac2b  10181  indpi  10964  genpcd  11063  ltexprlem7  11099  addcanpr  11103  reclem4pr  11107  suplem2pr  11110  sup2  12243  nnunb  12572  uzwo  13008  xrub  13412  grpid  19148  lsmcss  21960  uniopn  23177  fclsss1  24303  fclsss2  24304  ltsval2  27947  addonbday  28599  acycgrcycl  30687  grpoid  31056  spansncvi  32188  pjnormssi  32704  sumdmdlem2  32955  meran1  37121  bj-animbi  37350  currysetlem2  37783  bj-elsn0  37996  poimirlem31  38489  heicant  38493  disjimeceqim2  39657  hlhilhillem  42937  sn-sup2  43483  ee223  45561  eel2122old  45644  afv0nbfvbi  48143  fmtnoprmfac1lem  48571