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  3566  po2nr  5582  somo  5607  ordelord  6382  tz7.7  6386  funssres  6580  2elresin  6656  dffv2  6976  f1imass  7262  onint  7787  onfununi  8326  smoel  8345  tfrlem11  8373  tfr3  8384  omass  8563  nnmass  8608  sbthlem1  9073  pssnn  9151  php  9189  inf3lem2  9596  cardne  9958  dfac2b  10121  indpi  10898  genpcd  10997  ltexprlem7  11033  addcanpr  11037  reclem4pr  11041  suplem2pr  11044  sup2  12177  nnunb  12506  uzwo  12941  xrub  13344  grpid  19048  lsmcss  21853  uniopn  23065  fclsss1  24190  fclsss2  24191  ltsval2  27831  addonbday  28483  grpoid  30883  spansncvi  32015  pjnormssi  32531  sumdmdlem2  32782  acycgrcycl  35647  meran1  36950  bj-animbi  37179  currysetlem2  37612  bj-elsn0  37827  poimirlem31  38330  heicant  38334  disjimeceqim2  39482  hlhilhillem  42762  sn-sup2  43293  ee223  45371  eel2122old  45454  afv0nbfvbi  47916  fmtnoprmfac1lem  48344