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  3563  po2nr  5547  somo  5572  ordelord  6340  tz7.7  6344  funssres  6537  2elresin  6614  dffv2  6930  f1imass  7212  onint  7737  onfununi  8275  smoel  8294  tfrlem11  8321  tfr3  8332  omass  8509  nnmass  8554  sbthlem1  9019  pssnn  9097  php  9135  inf3lem2  9542  cardne  9881  dfac2b  10045  indpi  10822  genpcd  10921  ltexprlem7  10957  addcanpr  10961  reclem4pr  10965  suplem2pr  10968  sup2  12102  nnunb  12401  uzwo  12828  xrub  13231  grpid  18909  lsmcss  21651  uniopn  22845  fclsss1  23970  fclsss2  23971  sltval2  27628  addsonbday  28260  grpoid  30578  spansncvi  31710  pjnormssi  32226  sumdmdlem2  32477  acycgrcycl  35322  meran1  36586  bj-animbi  36734  currysetlem2  37124  bj-elsn0  37331  poimirlem31  37823  heicant  37827  disjimeceqim2  38977  hlhilhillem  42257  sn-sup2  42782  ee223  44911  eel2122old  44994  afv0nbfvbi  47433  fmtnoprmfac1lem  47846