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  3561  po2nr  5536  somo  5561  ordelord  6324  tz7.7  6328  funssres  6521  2elresin  6598  dffv2  6912  f1imass  7193  onint  7718  onfununi  8256  smoel  8275  tfrlem11  8302  tfr3  8313  omass  8490  nnmass  8534  sbthlem1  8995  pssnn  9073  php  9111  inf3lem2  9514  cardne  9850  dfac2b  10014  indpi  10790  genpcd  10889  ltexprlem7  10925  addcanpr  10929  reclem4pr  10933  suplem2pr  10936  sup2  12070  nnunb  12369  uzwo  12801  xrub  13203  grpid  18880  lsmcss  21622  uniopn  22805  fclsss1  23930  fclsss2  23931  sltval2  27588  grpoid  30490  spansncvi  31622  pjnormssi  32138  sumdmdlem2  32389  acycgrcycl  35159  meran1  36424  bj-animbi  36572  currysetlem2  36961  bj-elsn0  37168  poimirlem31  37670  heicant  37674  hlhilhillem  41978  sn-sup2  42503  ee223  44646  eel2122old  44729  afv0nbfvbi  47161  fmtnoprmfac1lem  47574