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  3608  po2nr  5611  somo  5635  ordelord  6408  tz7.7  6412  funssres  6612  2elresin  6690  dffv2  7004  f1imass  7284  onint  7810  wfrlem12OLD  8359  wfrlem14OLD  8361  onfununi  8380  smoel  8399  tfrlem11  8427  tfr3  8438  omass  8617  nnmass  8661  sbthlem1  9122  pssnn  9207  php  9245  phpOLD  9257  inf3lem2  9667  cardne  10003  dfac2b  10169  indpi  10945  genpcd  11044  ltexprlem7  11080  addcanpr  11084  reclem4pr  11088  suplem2pr  11091  sup2  12222  nnunb  12520  uzwo  12951  xrub  13351  grpid  19006  lsmcss  21728  uniopn  22919  fclsss1  24046  fclsss2  24047  sltval2  27716  grpoid  30549  spansncvi  31681  pjnormssi  32197  sumdmdlem2  32448  acycgrcycl  35132  meran1  36394  bj-animbi  36542  currysetlem2  36931  bj-elsn0  37138  poimirlem31  37638  heicant  37642  hlhilhillem  41947  sn-sup2  42478  ee223  44632  eel2122old  44716  afv0nbfvbi  47101  fmtnoprmfac1lem  47489