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  1050  ordunidif  6413  dff3  7097  tfindsg  7858  findsg  7895  brtpos  8232  omwordi  8557  omass  8566  nnmwordi  8622  pssnn  9154  frfi  9246  ixpiunwdom  9553  cantnfp1lem3  9650  infxpenlem  9998  infxp  10198  ackbij1lem16  10218  axpowndlem3  10585  pwfseqlem4a  10647  gchina  10685  prlem936  11033  supsrlem  11097  flflp1  13842  hashunx  14424  swrdccat3blem  14778  repswswrd  14823  sumss  15777  fsumss  15778  prodss  16003  fprodss  16004  ruclem2  16289  prmind2  16744  rpexp  16782  fermltl  16844  prmreclem5  16981  ramcl  17090  wunress  17310  divsfval  17602  efgsfo  19810  lt6abl  19966  gsumval3  19978  mdetunilem8  22757  ordtrest2lem  23341  ptpjpre1  23709  fbfinnfr  23979  filufint  24058  ptcmplem2  24191  cphsqrtcl3  25327  ovoliun  25645  voliunlem3  25692  volsup  25696  cxpsqrt  26849  amgm  27136  wilthlem2  27214  sqff1o  27327  chtublem  27356  bposlem1  27429  bposlem3  27431  ostth  27784  nosupbnd1lem1  27853  noinfbnd1lem1  27868  cutlt  28106  clwwisshclwwslemlem  30345  atdmd  32731  atmd2  32733  mdsymlem4  32739  ordtrest2NEWlem  34293  eulerpartlemb  34739  dvelimalcased  35444  dvelimexcased  35446  fineqvac  35510  fineqvnttrclselem1  35515  dfon2lem9  36262  nn0prpwlem  36814  axtcond  36970  bj-ismooredr2  37733  ltflcei  38240  poimirlem30  38282  lplnexllnN  40319  2llnjaN  40321  paddasslem14  40588  cdleme32le  41202  dgrsub2  43845  naddgeoa  44104  evenwodadd  47585  iccelpart  48165  lighneallem3  48342  lighneal  48346  prmringnzring  49085