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  3574  po2nr  5560  somo  5585  ordelord  6354  tz7.7  6358  funssres  6560  2elresin  6639  dffv2  6956  f1imass  7239  onint  7766  onfununi  8310  smoel  8329  tfrlem11  8356  tfr3  8367  omass  8544  nnmass  8588  sbthlem1  9051  pssnn  9132  php  9171  inf3lem2  9582  cardne  9918  dfac2b  10084  indpi  10860  genpcd  10959  ltexprlem7  10995  addcanpr  10999  reclem4pr  11003  suplem2pr  11006  sup2  12139  nnunb  12438  uzwo  12870  xrub  13272  grpid  18907  lsmcss  21601  uniopn  22784  fclsss1  23909  fclsss2  23910  sltval2  27568  grpoid  30449  spansncvi  31581  pjnormssi  32097  sumdmdlem2  32348  acycgrcycl  35134  meran1  36399  bj-animbi  36547  currysetlem2  36936  bj-elsn0  37143  poimirlem31  37645  heicant  37649  hlhilhillem  41954  sn-sup2  42479  ee223  44624  eel2122old  44707  afv0nbfvbi  47152  fmtnoprmfac1lem  47565