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  3527  po2nr  5456  somo  5479  ordelord  6191  tz7.7  6195  funssres  6379  2elresin  6451  dffv2  6747  f1imass  7014  onint  7509  wfrlem12  7976  wfrlem14  7978  onfununi  7988  smoel  8007  tfrlem11  8034  tfr3  8045  omass  8216  nnmass  8260  sbthlem1  8649  php  8723  pssnn  8738  inf3lem2  9125  cardne  9427  dfac2b  9590  indpi  10367  genpcd  10466  ltexprlem7  10502  addcanpr  10506  reclem4pr  10510  suplem2pr  10513  sup2  11633  nnunb  11930  uzwo  12351  xrub  12746  grpid  18206  lsmcss  20457  uniopn  21597  fclsss1  22722  fclsss2  22723  grpoid  28402  spansncvi  29534  pjnormssi  30050  sumdmdlem2  30301  acycgrcycl  32625  trpredrec  33324  sltval2  33424  meran1  34149  bj-animbi  34288  currysetlem2  34664  bj-elsn0  34850  poimirlem31  35368  heicant  35372  hlhilhillem  39536  sn-sup2  39936  ee223  41713  eel2122old  41797  afv0nbfvbi  44075  fmtnoprmfac1lem  44449