Theorem pm2.43d 53

Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 56 and pm2.43i 52. (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 22	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 45	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  loolin  111  rspct  3537  po2nr  5508  somo  5531  ordelord  6273  tz7.7  6277  funssres  6462  2elresin  6537  dffv2  6845  f1imass  7118  onint  7617  wfrlem12OLD  8122  wfrlem14OLD  8124  onfununi  8143  smoel  8162  tfrlem11  8190  tfr3  8201  omass  8373  nnmass  8417  sbthlem1  8823  php  8897  pssnn  8913  inf3lem2  9317  trpredrec  9415  cardne  9654  dfac2b  9817  indpi  10594  genpcd  10693  ltexprlem7  10729  addcanpr  10733  reclem4pr  10737  suplem2pr  10740  sup2  11861  nnunb  12159  uzwo  12580  xrub  12975  grpid  18530  lsmcss  20809  uniopn  21954  fclsss1  23081  fclsss2  23082  grpoid  28783  spansncvi  29915  pjnormssi  30431  sumdmdlem2  30682  acycgrcycl  33009  sltval2  33786  meran1  34527  bj-animbi  34666  currysetlem2  35064  bj-elsn0  35253  poimirlem31  35735  heicant  35739  hlhilhillem  39905  sn-sup2  40360  ee223  42143  eel2122old  42227  afv0nbfvbi  44530  fmtnoprmfac1lem  44904