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  3564  po2nr  5554  somo  5579  ordelord  6347  tz7.7  6351  funssres  6544  2elresin  6621  dffv2  6937  f1imass  7220  onint  7745  onfununi  8283  smoel  8302  tfrlem11  8329  tfr3  8340  omass  8517  nnmass  8562  sbthlem1  9027  pssnn  9105  php  9143  inf3lem2  9550  cardne  9889  dfac2b  10053  indpi  10830  genpcd  10929  ltexprlem7  10965  addcanpr  10969  reclem4pr  10973  suplem2pr  10976  sup2  12110  nnunb  12409  uzwo  12836  xrub  13239  grpid  18917  lsmcss  21659  uniopn  22853  fclsss1  23978  fclsss2  23979  ltsval2  27636  addonbday  28287  grpoid  30607  spansncvi  31739  pjnormssi  32255  sumdmdlem2  32506  acycgrcycl  35360  meran1  36624  bj-animbi  36780  currysetlem2  37187  bj-elsn0  37399  poimirlem31  37891  heicant  37895  disjimeceqim2  39045  hlhilhillem  42325  sn-sup2  42850  ee223  44979  eel2122old  45062  afv0nbfvbi  47500  fmtnoprmfac1lem  47913