Theorem pm2.43d 51

Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 54 and pm2.43i 50. (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 44	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  109  rspct  3275  po2nr  4972  somo  4993  ordelord  5662  tz7.7  5666  funssres  5844  2elresin  5916  dffv2  6181  f1imass  6422  onint  6887  wfrlem12  7313  wfrlem14  7315  onfununi  7325  smoel  7344  tfrlem11  7371  tfr3  7382  omass  7547  nnmass  7591  sbthlem1  7955  php  8029  inf3lem2  8409  cardne  8674  dfac2  8836  indpi  9608  genpcd  9707  ltexprlem7  9743  addcanpr  9747  reclem4pr  9751  suplem2pr  9754  sup2  10858  nnunb  11165  uzwo  11627  xrub  12014  grpid  17280  lsmcss  19855  uniopn  20527  fclsss1  21636  fclsss2  21637  0clwlk  26293  frg2wot1  26584  grpoid  26758  spansncvi  27895  pjnormssi  28411  sumdmdlem2  28662  trpredrec  30982  frrlem11  31036  sltval2  31053  nobndup  31099  nobnddown  31100  meran1  31580  poimirlem31  32610  heicant  32614  hlhilhillem  36270  ee223  37880  eel2122old  37964  afv0nbfvbi  39880  frgr2wwlk1  41494