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  3593  po2nr  5598  somo  5621  ordelord  6385  tz7.7  6389  funssres  6591  2elresin  6670  dffv2  6987  f1imass  7268  onint  7787  wfrlem12OLD  8334  wfrlem14OLD  8336  onfununi  8355  smoel  8374  tfrlem11  8402  tfr3  8413  omass  8594  nnmass  8638  sbthlem1  9099  pssnn  9184  php  9226  phpOLD  9238  inf3lem2  9644  cardne  9980  dfac2b  10145  indpi  10922  genpcd  11021  ltexprlem7  11057  addcanpr  11061  reclem4pr  11065  suplem2pr  11068  sup2  12192  nnunb  12490  uzwo  12917  xrub  13315  grpid  18923  lsmcss  21611  uniopn  22786  fclsss1  23913  fclsss2  23914  sltval2  27576  grpoid  30317  spansncvi  31449  pjnormssi  31965  sumdmdlem2  32216  acycgrcycl  34693  meran1  35831  bj-animbi  35970  currysetlem2  36363  bj-elsn0  36570  poimirlem31  37059  heicant  37063  hlhilhillem  41374  sn-sup2  41946  ee223  43996  eel2122old  44080  afv0nbfvbi  46454  fmtnoprmfac1lem  46827