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  6432  dff3  7119  tfindsg  7883  findsg  7920  brtpos  8261  omwordi  8610  omass  8619  nnmwordi  8674  pssnn  9209  frfi  9322  ixpiunwdom  9631  cantnfp1lem3  9721  infxpenlem  10054  infxp  10255  ackbij1lem16  10275  axpowndlem3  10640  pwfseqlem4a  10702  gchina  10740  prlem936  11088  supsrlem  11152  flflp1  13848  hashunx  14426  swrdccat3blem  14778  repswswrd  14823  sumss  15761  fsumss  15762  prodss  15984  fprodss  15985  ruclem2  16269  prmind2  16723  rpexp  16760  fermltl  16822  prmreclem5  16959  ramcl  17068  wunress  17296  wunressOLD  17297  divsfval  17593  efgsfo  19758  lt6abl  19914  gsumval3  19926  mdetunilem8  22626  ordtrest2lem  23212  ptpjpre1  23580  fbfinnfr  23850  filufint  23929  ptcmplem2  24062  cphsqrtcl3  25222  ovoliun  25541  voliunlem3  25588  volsup  25592  cxpsqrt  26746  amgm  27035  wilthlem2  27113  sqff1o  27226  chtublem  27256  bposlem1  27329  bposlem3  27331  ostth  27684  nosupbnd1lem1  27754  noinfbnd1lem1  27769  cutlt  27967  clwwisshclwwslemlem  30033  atdmd  32418  atmd2  32420  mdsymlem4  32426  ordtrest2NEWlem  33922  eulerpartlemb  34371  dvelimalcased  35090  dvelimexcased  35092  fineqvac  35112  dfon2lem9  35793  nn0prpwlem  36324  bj-ismooredr2  37112  ltflcei  37616  poimirlem30  37658  lplnexllnN  39567  2llnjaN  39569  paddasslem14  39836  cdleme32le  40450  dgrsub2  43152  naddgeoa  43412  evenwodadd  46908  iccelpart  47425  lighneallem3  47599  lighneal  47603