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  3577  po2nr  5562  somo  5587  ordelord  6356  tz7.7  6360  funssres  6562  2elresin  6641  dffv2  6958  f1imass  7241  onint  7768  onfununi  8312  smoel  8331  tfrlem11  8358  tfr3  8369  omass  8546  nnmass  8590  sbthlem1  9056  pssnn  9137  php  9176  inf3lem2  9588  cardne  9924  dfac2b  10090  indpi  10866  genpcd  10965  ltexprlem7  11001  addcanpr  11005  reclem4pr  11009  suplem2pr  11012  sup2  12145  nnunb  12444  uzwo  12876  xrub  13278  grpid  18913  lsmcss  21607  uniopn  22790  fclsss1  23915  fclsss2  23916  sltval2  27574  grpoid  30455  spansncvi  31587  pjnormssi  32103  sumdmdlem2  32354  acycgrcycl  35134  meran1  36394  bj-animbi  36542  currysetlem2  36931  bj-elsn0  37138  poimirlem31  37640  heicant  37644  hlhilhillem  41949  sn-sup2  42472  ee223  44617  eel2122old  44700  afv0nbfvbi  47142  fmtnoprmfac1lem  47555