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  3593  po2nr  5603  somo  5626  ordelord  6391  tz7.7  6395  funssres  6596  2elresin  6675  dffv2  6990  f1imass  7272  onint  7792  wfrlem12OLD  8339  wfrlem14OLD  8341  onfununi  8360  smoel  8379  tfrlem11  8407  tfr3  8418  omass  8599  nnmass  8643  sbthlem1  9106  pssnn  9191  php  9233  phpOLD  9245  inf3lem2  9652  cardne  9988  dfac2b  10153  indpi  10930  genpcd  11029  ltexprlem7  11065  addcanpr  11069  reclem4pr  11073  suplem2pr  11076  sup2  12200  nnunb  12498  uzwo  12925  xrub  13323  grpid  18937  lsmcss  21629  uniopn  22830  fclsss1  23957  fclsss2  23958  sltval2  27620  grpoid  30387  spansncvi  31519  pjnormssi  32035  sumdmdlem2  32286  acycgrcycl  34844  meran1  35982  bj-animbi  36121  currysetlem2  36514  bj-elsn0  36721  poimirlem31  37211  heicant  37215  hlhilhillem  41523  sn-sup2  42106  ee223  44155  eel2122old  44239  afv0nbfvbi  46611  fmtnoprmfac1lem  46983