Theorem pm2.43d 54

Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 57 and pm2.43i 53. (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 23	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 46	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  112  rspct  3570  po2nr  5574  somo  5599  ordelord  6372  tz7.7  6376  funssres  6569  2elresin  6646  dffv2  6966  f1imass  7252  onint  7777  onfununi  8316  smoel  8335  tfrlem11  8363  tfr3  8374  omass  8553  nnmass  8598  sbthlem1  9063  pssnn  9141  php  9179  inf3lem2  9586  cardne  9939  dfac2b  10102  indpi  10880  genpcd  10979  ltexprlem7  11015  addcanpr  11019  reclem4pr  11023  suplem2pr  11026  sup2  12162  nnunb  12491  uzwo  12926  xrub  13329  grpid  19032  lsmcss  21802  uniopn  23015  fclsss1  24140  fclsss2  24141  ltsval2  27778  addonbday  28430  grpoid  30781  spansncvi  31913  pjnormssi  32429  sumdmdlem2  32680  acycgrcycl  35510  meran1  36784  bj-animbi  37013  currysetlem2  37445  bj-elsn0  37659  poimirlem31  38162  heicant  38166  disjimeceqim2  39316  hlhilhillem  42596  sn-sup2  43125  ee223  45208  eel2122old  45291  afv0nbfvbi  47743  fmtnoprmfac1lem  48171