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  110  rspct  3442  po2nr  5200  somo  5221  ordelord  5906  tz7.7  5910  funssres  6091  2elresin  6163  dffv2  6434  f1imass  6685  onint  7161  wfrlem12  7596  wfrlem14  7598  onfununi  7608  smoel  7627  tfrlem11  7654  tfr3  7665  omass  7831  nnmass  7875  sbthlem1  8237  php  8311  inf3lem2  8701  cardne  9001  dfac2b  9163  dfac2OLD  9165  indpi  9941  genpcd  10040  ltexprlem7  10076  addcanpr  10080  reclem4pr  10084  suplem2pr  10087  sup2  11191  nnunb  11500  uzwo  11964  xrub  12355  grpid  17678  lsmcss  20258  uniopn  20924  fclsss1  22047  fclsss2  22048  grpoid  27704  spansncvi  28841  pjnormssi  29357  sumdmdlem2  29608  trpredrec  32064  sltval2  32136  meran1  32737  poimirlem31  33771  heicant  33775  hlhilhillem  37772  ee223  39379  eel2122old  39463  afv0nbfvbi  41755  fmtnoprmfac1lem  42004