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  3621  po2nr  5622  somo  5646  ordelord  6417  tz7.7  6421  funssres  6622  2elresin  6701  dffv2  7017  f1imass  7301  onint  7826  wfrlem12OLD  8376  wfrlem14OLD  8378  onfununi  8397  smoel  8416  tfrlem11  8444  tfr3  8455  omass  8636  nnmass  8680  sbthlem1  9149  pssnn  9234  php  9273  phpOLD  9285  inf3lem2  9698  cardne  10034  dfac2b  10200  indpi  10976  genpcd  11075  ltexprlem7  11111  addcanpr  11115  reclem4pr  11119  suplem2pr  11122  sup2  12251  nnunb  12549  uzwo  12976  xrub  13374  grpid  19015  lsmcss  21733  uniopn  22924  fclsss1  24051  fclsss2  24052  sltval2  27719  grpoid  30552  spansncvi  31684  pjnormssi  32200  sumdmdlem2  32451  acycgrcycl  35115  meran1  36377  bj-animbi  36525  currysetlem2  36914  bj-elsn0  37121  poimirlem31  37611  heicant  37615  hlhilhillem  41921  sn-sup2  42447  ee223  44605  eel2122old  44689  afv0nbfvbi  47066  fmtnoprmfac1lem  47438