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  5572  somo  5597  ordelord  6384  tz7.7  6388  funssres  6584  2elresin  6660  dffv2  6980  f1imass  7268  onint  7804  onfununi  8350  smoel  8369  tfrlem11  8397  tfr3  8408  omass  8589  nnmass  8634  sbthlem1  9107  pssnn  9185  php  9223  inf3lem2  9631  cardne  10047  dfac2b  10210  indpi  10993  genpcd  11092  ltexprlem7  11128  addcanpr  11132  reclem4pr  11136  suplem2pr  11139  sup2  12274  nnunb  12603  uzwo  13039  xrub  13443  grpid  19187  lsmcss  21999  uniopn  23216  fclsss1  24342  fclsss2  24343  ltsval2  28014  addonbday  28666  acycgrcycl  30754  grpoid  31123  spansncvi  32255  pjnormssi  32771  sumdmdlem2  33022  meran1  37242  bj-animbi  37471  currysetlem2  37904  bj-elsn0  38120  poimirlem31  38613  heicant  38617  disjimeceqim2  39781  hlhilhillem  43061  sn-sup2  43599  ee223  45661  eel2122old  45744  afv0nbfvbi  48265  fmtnoprmfac1lem  48693