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  379  bija  380  pm2.61dan  812  ecase3d  1034  ordunidif  6367  dff3  7045  tfindsg  7803  findsg  7839  brtpos  8177  omwordi  8498  omass  8507  nnmwordi  8563  pssnn  9093  frfi  9185  ixpiunwdom  9495  cantnfp1lem3  9589  infxpenlem  9923  infxp  10124  ackbij1lem16  10144  axpowndlem3  10510  pwfseqlem4a  10572  gchina  10610  prlem936  10958  supsrlem  11022  flflp1  13727  hashunx  14309  swrdccat3blem  14662  repswswrd  14707  sumss  15647  fsumss  15648  prodss  15870  fprodss  15871  ruclem2  16157  prmind2  16612  rpexp  16649  fermltl  16711  prmreclem5  16848  ramcl  16957  wunress  17176  divsfval  17468  efgsfo  19668  lt6abl  19824  gsumval3  19836  mdetunilem8  22563  ordtrest2lem  23147  ptpjpre1  23515  fbfinnfr  23785  filufint  23864  ptcmplem2  23997  cphsqrtcl3  25143  ovoliun  25462  voliunlem3  25509  volsup  25513  cxpsqrt  26668  amgm  26957  wilthlem2  27035  sqff1o  27148  chtublem  27178  bposlem1  27251  bposlem3  27253  ostth  27606  nosupbnd1lem1  27676  noinfbnd1lem1  27691  cutlt  27928  clwwisshclwwslemlem  30088  atdmd  32473  atmd2  32475  mdsymlem4  32481  ordtrest2NEWlem  34079  eulerpartlemb  34525  dvelimalcased  35231  dvelimexcased  35233  fineqvac  35272  fineqvnttrclselem1  35277  dfon2lem9  35983  nn0prpwlem  36516  bj-ismooredr2  37311  ltflcei  37805  poimirlem30  37847  lplnexllnN  39820  2llnjaN  39822  paddasslem14  40089  cdleme32le  40703  dgrsub2  43373  naddgeoa  43632  evenwodadd  47127  iccelpart  47675  lighneallem3  47849  lighneal  47853