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  3565  po2nr  5545  somo  5570  ordelord  6333  tz7.7  6337  funssres  6530  2elresin  6607  dffv2  6922  f1imass  7205  onint  7730  onfununi  8271  smoel  8290  tfrlem11  8317  tfr3  8328  omass  8505  nnmass  8549  sbthlem1  9011  pssnn  9092  php  9131  inf3lem2  9544  cardne  9880  dfac2b  10044  indpi  10820  genpcd  10919  ltexprlem7  10955  addcanpr  10959  reclem4pr  10963  suplem2pr  10966  sup2  12099  nnunb  12398  uzwo  12830  xrub  13232  grpid  18872  lsmcss  21617  uniopn  22800  fclsss1  23925  fclsss2  23926  sltval2  27584  grpoid  30482  spansncvi  31614  pjnormssi  32130  sumdmdlem2  32381  acycgrcycl  35119  meran1  36384  bj-animbi  36532  currysetlem2  36921  bj-elsn0  37128  poimirlem31  37630  heicant  37634  hlhilhillem  41939  sn-sup2  42464  ee223  44608  eel2122old  44691  afv0nbfvbi  47136  fmtnoprmfac1lem  47549