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  5577  somo  5602  ordelord  6402  tz7.7  6406  funssres  6604  2elresin  6682  dffv2  7003  f1imass  7291  onint  7828  onfununi  8377  smoel  8396  tfrlem11  8424  tfr3  8435  omass  8616  nnmass  8661  sbthlem1  9134  pssnn  9212  php  9250  inf3lem2  9657  cardne  10073  dfac2b  10236  indpi  11019  genpcd  11118  ltexprlem7  11154  addcanpr  11158  reclem4pr  11162  suplem2pr  11165  sup2  12300  nnunb  12629  uzwo  13065  xrub  13469  grpid  19215  lsmcss  22028  uniopn  23245  fclsss1  24371  fclsss2  24372  ltsval2  28043  addonbday  28695  acycgrcycl  30783  grpoid  31152  spansncvi  32284  pjnormssi  32800  sumdmdlem2  33051  meran1  37377  bj-animbi  37606  currysetlem2  38039  bj-elsn0  38268  poimirlem31  38761  heicant  38765  disjimeceqim2  39929  hlhilhillem  43209  sn-sup2  43748  ee223  45808  eel2122old  45891  afv0nbfvbi  48426  fmtnoprmfac1lem  48854