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  3565  po2nr  5581  somo  5606  ordelord  6383  tz7.7  6387  funssres  6581  2elresin  6657  dffv2  6977  f1imass  7264  onint  7792  onfununi  8333  smoel  8352  tfrlem11  8380  tfr3  8391  omass  8570  nnmass  8615  sbthlem1  9088  pssnn  9166  php  9204  inf3lem2  9611  cardne  9973  dfac2b  10136  indpi  10919  genpcd  11018  ltexprlem7  11054  addcanpr  11058  reclem4pr  11062  suplem2pr  11065  sup2  12198  nnunb  12527  uzwo  12963  xrub  13366  grpid  19103  lsmcss  21909  uniopn  23126  fclsss1  24252  fclsss2  24253  ltsval2  27893  addonbday  28545  acycgrcycl  30633  grpoid  31002  spansncvi  32134  pjnormssi  32650  sumdmdlem2  32901  meran1  37032  bj-animbi  37261  currysetlem2  37694  bj-elsn0  37909  poimirlem31  38402  heicant  38406  disjimeceqim2  39555  hlhilhillem  42835  sn-sup2  43381  ee223  45459  eel2122old  45542  afv0nbfvbi  48041  fmtnoprmfac1lem  48469