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  3567  po2nr  5559  somo  5582  ordelord  6339  tz7.7  6343  funssres  6545  2elresin  6622  dffv2  6936  f1imass  7210  onint  7724  wfrlem12OLD  8265  wfrlem14OLD  8267  onfununi  8286  smoel  8305  tfrlem11  8333  tfr3  8344  omass  8526  nnmass  8570  sbthlem1  9026  pssnn  9111  php  9153  phpOLD  9165  inf3lem2  9564  cardne  9900  dfac2b  10065  indpi  10842  genpcd  10941  ltexprlem7  10977  addcanpr  10981  reclem4pr  10985  suplem2pr  10988  sup2  12110  nnunb  12408  uzwo  12835  xrub  13230  grpid  18785  lsmcss  21094  uniopn  22244  fclsss1  23371  fclsss2  23372  sltval2  27002  grpoid  29409  spansncvi  30541  pjnormssi  31057  sumdmdlem2  31308  acycgrcycl  33681  meran1  34873  bj-animbi  35012  currysetlem2  35409  bj-elsn0  35616  poimirlem31  36099  heicant  36103  hlhilhillem  40417  sn-sup2  40915  ee223  42897  eel2122old  42981  afv0nbfvbi  45354  fmtnoprmfac1lem  45727