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  3592  po2nr  5580  somo  5605  ordelord  6379  tz7.7  6383  funssres  6585  2elresin  6664  dffv2  6979  f1imass  7262  onint  7789  wfrlem12OLD  8339  wfrlem14OLD  8341  onfununi  8360  smoel  8379  tfrlem11  8407  tfr3  8418  omass  8597  nnmass  8641  sbthlem1  9102  pssnn  9187  php  9226  phpOLD  9236  inf3lem2  9648  cardne  9984  dfac2b  10150  indpi  10926  genpcd  11025  ltexprlem7  11061  addcanpr  11065  reclem4pr  11069  suplem2pr  11072  sup2  12203  nnunb  12502  uzwo  12932  xrub  13333  grpid  18963  lsmcss  21657  uniopn  22840  fclsss1  23965  fclsss2  23966  sltval2  27625  grpoid  30506  spansncvi  31638  pjnormssi  32154  sumdmdlem2  32405  acycgrcycl  35174  meran1  36434  bj-animbi  36582  currysetlem2  36971  bj-elsn0  37178  poimirlem31  37680  heicant  37684  hlhilhillem  41984  sn-sup2  42481  ee223  44626  eel2122old  44709  afv0nbfvbi  47147  fmtnoprmfac1lem  47545