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  5601  somo  5624  ordelord  6383  tz7.7  6387  funssres  6589  2elresin  6668  dffv2  6983  f1imass  7259  onint  7774  wfrlem12OLD  8316  wfrlem14OLD  8318  onfununi  8337  smoel  8356  tfrlem11  8384  tfr3  8395  omass  8576  nnmass  8620  sbthlem1  9079  pssnn  9164  php  9206  phpOLD  9218  inf3lem2  9620  cardne  9956  dfac2b  10121  indpi  10898  genpcd  10997  ltexprlem7  11033  addcanpr  11037  reclem4pr  11041  suplem2pr  11044  sup2  12166  nnunb  12464  uzwo  12891  xrub  13287  grpid  18856  lsmcss  21236  uniopn  22390  fclsss1  23517  fclsss2  23518  sltval2  27148  grpoid  29760  spansncvi  30892  pjnormssi  31408  sumdmdlem2  31659  acycgrcycl  34126  meran1  35284  bj-animbi  35423  currysetlem2  35817  bj-elsn0  36024  poimirlem31  36507  heicant  36511  hlhilhillem  40823  sn-sup2  41338  ee223  43380  eel2122old  43464  afv0nbfvbi  45845  fmtnoprmfac1lem  46218