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  3557  po2nr  5451  somo  5474  ordelord  6181  tz7.7  6185  funssres  6368  2elresin  6440  dffv2  6733  f1imass  7000  onint  7490  wfrlem12  7949  wfrlem14  7951  onfununi  7961  smoel  7980  tfrlem11  8007  tfr3  8018  omass  8189  nnmass  8233  sbthlem1  8611  php  8685  inf3lem2  9076  cardne  9378  dfac2b  9541  indpi  10318  genpcd  10417  ltexprlem7  10453  addcanpr  10457  reclem4pr  10461  suplem2pr  10464  sup2  11584  nnunb  11881  uzwo  12299  xrub  12693  grpid  18131  lsmcss  20381  uniopn  21502  fclsss1  22627  fclsss2  22628  grpoid  28303  spansncvi  29435  pjnormssi  29951  sumdmdlem2  30202  acycgrcycl  32507  trpredrec  33190  sltval2  33276  meran1  33872  bj-animbi  34007  currysetlem2  34383  bj-elsn0  34570  poimirlem31  35088  heicant  35092  hlhilhillem  39256  sn-sup2  39594  ee223  41340  eel2122old  41424  afv0nbfvbi  43707  fmtnoprmfac1lem  44081