Theorem pm2.61d 181

Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61d.1	⊢ (𝜑 → (𝜓 → 𝜒))
pm2.61d.2	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
pm2.61d	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.2	. . . 4 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2	1	con1d 146	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 48	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 128	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.61d1  182  pm2.61d2  183  pm5.21ndd  382  bija  383  pm2.61dan  824  ecase3d  1048  ordunidif  6400  dff3  7085  tfindsg  7845  findsg  7882  brtpos  8219  omwordi  8544  omass  8553  nnmwordi  8609  pssnn  9141  frfi  9233  ixpiunwdom  9540  cantnfp1lem3  9637  infxpenlem  9985  infxp  10185  ackbij1lem16  10205  axpowndlem3  10572  pwfseqlem4a  10634  gchina  10672  prlem936  11020  supsrlem  11084  flflp1  13828  hashunx  14410  swrdccat3blem  14764  repswswrd  14809  sumss  15763  fsumss  15764  prodss  15989  fprodss  15990  ruclem2  16276  prmind2  16731  rpexp  16769  fermltl  16831  prmreclem5  16968  ramcl  17077  wunress  17297  divsfval  17589  efgsfo  19797  lt6abl  19953  gsumval3  19965  mdetunilem8  22733  ordtrest2lem  23317  ptpjpre1  23685  fbfinnfr  23955  filufint  24034  ptcmplem2  24167  cphsqrtcl3  25303  ovoliun  25621  voliunlem3  25668  volsup  25672  cxpsqrt  26822  amgm  27109  wilthlem2  27187  sqff1o  27300  chtublem  27329  bposlem1  27402  bposlem3  27404  ostth  27757  nosupbnd1lem1  27826  noinfbnd1lem1  27841  cutlt  28079  clwwisshclwwslemlem  30269  atdmd  32655  atmd2  32657  mdsymlem4  32663  ordtrest2NEWlem  34224  eulerpartlemb  34670  dvelimalcased  35375  dvelimexcased  35377  fineqvac  35419  fineqvnttrclselem1  35424  dfon2lem9  36147  nn0prpwlem  36690  axtcond  36846  bj-ismooredr2  37607  ltflcei  38114  poimirlem30  38156  lplnexllnN  40195  2llnjaN  40197  paddasslem14  40464  cdleme32le  41078  dgrsub2  43719  naddgeoa  43978  evenwodadd  47462  iccelpart  48038  lighneallem3  48215  lighneal  48219  prmringnzring  48958