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  3553  po2nr  5547  somo  5572  ordelord  6339  tz7.7  6343  funssres  6536  2elresin  6613  dffv2  6929  f1imass  7215  onint  7740  onfununi  8278  smoel  8297  tfrlem11  8324  tfr3  8335  omass  8512  nnmass  8557  sbthlem1  9022  pssnn  9100  php  9138  inf3lem2  9548  cardne  9887  dfac2b  10051  indpi  10828  genpcd  10927  ltexprlem7  10963  addcanpr  10967  reclem4pr  10971  suplem2pr  10974  sup2  12110  nnunb  12431  uzwo  12859  xrub  13262  grpid  18949  lsmcss  21674  uniopn  22887  fclsss1  24012  fclsss2  24013  ltsval2  27645  addonbday  28296  grpoid  30616  spansncvi  31748  pjnormssi  32264  sumdmdlem2  32515  acycgrcycl  35376  meran1  36640  bj-animbi  36870  currysetlem2  37302  bj-elsn0  37516  poimirlem31  38019  heicant  38023  disjimeceqim2  39173  hlhilhillem  42453  sn-sup2  42982  ee223  45079  eel2122old  45162  afv0nbfvbi  47615  fmtnoprmfac1lem  48043