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  3598  po2nr  5602  somo  5625  ordelord  6386  tz7.7  6390  funssres  6592  2elresin  6671  dffv2  6986  f1imass  7265  onint  7780  wfrlem12OLD  8322  wfrlem14OLD  8324  onfununi  8343  smoel  8362  tfrlem11  8390  tfr3  8401  omass  8582  nnmass  8626  sbthlem1  9085  pssnn  9170  php  9212  phpOLD  9224  inf3lem2  9626  cardne  9962  dfac2b  10127  indpi  10904  genpcd  11003  ltexprlem7  11039  addcanpr  11043  reclem4pr  11047  suplem2pr  11050  sup2  12174  nnunb  12472  uzwo  12899  xrub  13295  grpid  18896  lsmcss  21464  uniopn  22619  fclsss1  23746  fclsss2  23747  sltval2  27383  grpoid  30028  spansncvi  31160  pjnormssi  31676  sumdmdlem2  31927  acycgrcycl  34424  meran1  35599  bj-animbi  35738  currysetlem2  36132  bj-elsn0  36339  poimirlem31  36822  heicant  36826  hlhilhillem  41138  sn-sup2  41644  ee223  43697  eel2122old  43781  afv0nbfvbi  46158  fmtnoprmfac1lem  46531