Theorem pm2.61d 179

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 145	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 47	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 127	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  180  pm2.61d2  181  pm5.21ndd  381  bija  382  pm2.61dan  810  ecase3d  1031  ordunidif  6314  dff3  6976  tfindsg  7707  findsg  7746  brtpos  8051  omwordi  8402  omass  8411  nnmwordi  8466  pssnn  8951  pssnnOLD  9040  frfi  9059  ixpiunwdom  9349  cantnfp1lem3  9438  infxpenlem  9769  infxp  9971  ackbij1lem16  9991  axpowndlem3  10355  pwfseqlem4a  10417  gchina  10455  prlem936  10803  supsrlem  10867  flflp1  13527  hashunx  14101  swrdccat3blem  14452  repswswrd  14497  sumss  15436  fsumss  15437  prodss  15657  fprodss  15658  ruclem2  15941  prmind2  16390  rpexp  16427  fermltl  16485  prmreclem5  16621  ramcl  16730  wunress  16960  wunressOLD  16961  divsfval  17258  efgsfo  19345  lt6abl  19496  gsumval3  19508  mdetunilem8  21768  ordtrest2lem  22354  ptpjpre1  22722  fbfinnfr  22992  filufint  23071  ptcmplem2  23204  cphsqrtcl3  24351  ovoliun  24669  voliunlem3  24716  volsup  24720  cxpsqrt  25858  amgm  26140  wilthlem2  26218  sqff1o  26331  chtublem  26359  bposlem1  26432  bposlem3  26434  ostth  26787  clwwisshclwwslemlem  28377  atdmd  30760  atmd2  30762  mdsymlem4  30768  ordtrest2NEWlem  31872  eulerpartlemb  32335  fineqvac  33066  dfon2lem9  33767  nosupbnd1lem1  33911  noinfbnd1lem1  33926  nn0prpwlem  34511  bj-ismooredr2  35281  ltflcei  35765  poimirlem30  35807  lplnexllnN  37578  2llnjaN  37580  paddasslem14  37847  cdleme32le  38461  dgrsub2  40960  iccelpart  44885  lighneallem3  45059  lighneal  45063