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  3560  po2nr  5543  somo  5568  ordelord  6336  tz7.7  6340  funssres  6533  2elresin  6610  dffv2  6926  f1imass  7207  onint  7732  onfununi  8270  smoel  8289  tfrlem11  8316  tfr3  8327  omass  8504  nnmass  8548  sbthlem1  9010  pssnn  9088  php  9126  inf3lem2  9529  cardne  9868  dfac2b  10032  indpi  10808  genpcd  10907  ltexprlem7  10943  addcanpr  10947  reclem4pr  10951  suplem2pr  10954  sup2  12088  nnunb  12387  uzwo  12819  xrub  13221  grpid  18898  lsmcss  21639  uniopn  22822  fclsss1  23947  fclsss2  23948  sltval2  27605  grpoid  30511  spansncvi  31643  pjnormssi  32159  sumdmdlem2  32410  acycgrcycl  35202  meran1  36466  bj-animbi  36614  currysetlem2  37003  bj-elsn0  37210  poimirlem31  37701  heicant  37705  hlhilhillem  42069  sn-sup2  42599  ee223  44741  eel2122old  44824  afv0nbfvbi  47265  fmtnoprmfac1lem  47678