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  3562  po2nr  5562  somo  5587  ordelord  6357  tz7.7  6361  funssres  6554  2elresin  6631  dffv2  6951  f1imass  7237  onint  7762  onfununi  8300  smoel  8319  tfrlem11  8347  tfr3  8358  omass  8537  nnmass  8582  sbthlem1  9048  pssnn  9126  php  9164  inf3lem2  9574  cardne  9913  dfac2b  10077  indpi  10855  genpcd  10954  ltexprlem7  10990  addcanpr  10994  reclem4pr  10998  suplem2pr  11001  sup2  12138  nnunb  12467  uzwo  12902  xrub  13305  grpid  18993  lsmcss  21717  uniopn  22930  fclsss1  24055  fclsss2  24056  ltsval2  27690  addonbday  28342  grpoid  30662  spansncvi  31794  pjnormssi  32310  sumdmdlem2  32561  acycgrcycl  35445  meran1  36719  bj-animbi  36949  currysetlem2  37381  bj-elsn0  37595  poimirlem31  38098  heicant  38102  disjimeceqim2  39252  hlhilhillem  42532  sn-sup2  43061  ee223  45158  eel2122old  45241  afv0nbfvbi  47693  fmtnoprmfac1lem  48121