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  13831  hashunx  14413  swrdccat3blem  14766  repswswrd  14811  sumss  15765  fsumss  15766  prodss  15991  fprodss  15992  ruclem2  16278  prmind2  16733  rpexp  16771  fermltl  16833  prmreclem5  16970  ramcl  17079  wunress  17299  divsfval  17591  efgsfo  19800  lt6abl  19956  gsumval3  19968  mdetunilem8  22737  ordtrest2lem  23321  ptpjpre1  23689  fbfinnfr  23959  filufint  24038  ptcmplem2  24171  cphsqrtcl3  25307  ovoliun  25625  voliunlem3  25672  volsup  25676  cxpsqrt  26826  amgm  27113  wilthlem2  27191  sqff1o  27304  chtublem  27333  bposlem1  27406  bposlem3  27408  ostth  27761  nosupbnd1lem1  27830  noinfbnd1lem1  27845  cutlt  28083  clwwisshclwwslemlem  30273  atdmd  32659  atmd2  32661  mdsymlem4  32667  ordtrest2NEWlem  34229  eulerpartlemb  34675  dvelimalcased  35380  dvelimexcased  35382  fineqvac  35424  fineqvnttrclselem1  35429  dfon2lem9  36152  nn0prpwlem  36695  axtcond  36851  bj-ismooredr2  37612  ltflcei  38119  poimirlem30  38161  lplnexllnN  40200  2llnjaN  40202  paddasslem14  40469  cdleme32le  41083  dgrsub2  43724  naddgeoa  43983  evenwodadd  47461  iccelpart  48037  lighneallem3  48214  lighneal  48218  prmringnzring  48957