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  3608  po2nr  5606  somo  5631  ordelord  6406  tz7.7  6410  funssres  6610  2elresin  6689  dffv2  7004  f1imass  7284  onint  7810  wfrlem12OLD  8360  wfrlem14OLD  8362  onfununi  8381  smoel  8400  tfrlem11  8428  tfr3  8439  omass  8618  nnmass  8662  sbthlem1  9123  pssnn  9208  php  9247  phpOLD  9259  inf3lem2  9669  cardne  10005  dfac2b  10171  indpi  10947  genpcd  11046  ltexprlem7  11082  addcanpr  11086  reclem4pr  11090  suplem2pr  11093  sup2  12224  nnunb  12522  uzwo  12953  xrub  13354  grpid  18993  lsmcss  21710  uniopn  22903  fclsss1  24030  fclsss2  24031  sltval2  27701  grpoid  30539  spansncvi  31671  pjnormssi  32187  sumdmdlem2  32438  acycgrcycl  35152  meran1  36412  bj-animbi  36560  currysetlem2  36949  bj-elsn0  37156  poimirlem31  37658  heicant  37662  hlhilhillem  41966  sn-sup2  42501  ee223  44654  eel2122old  44738  afv0nbfvbi  47163  fmtnoprmfac1lem  47551