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  6356  dff3  7033  tfindsg  7791  findsg  7827  brtpos  8165  omwordi  8486  omass  8495  nnmwordi  8550  pssnn  9078  frfi  9169  ixpiunwdom  9476  cantnfp1lem3  9570  infxpenlem  9901  infxp  10102  ackbij1lem16  10122  axpowndlem3  10487  pwfseqlem4a  10549  gchina  10587  prlem936  10935  supsrlem  10999  flflp1  13708  hashunx  14290  swrdccat3blem  14643  repswswrd  14688  sumss  15628  fsumss  15629  prodss  15851  fprodss  15852  ruclem2  16138  prmind2  16593  rpexp  16630  fermltl  16692  prmreclem5  16829  ramcl  16938  wunress  17157  divsfval  17448  efgsfo  19649  lt6abl  19805  gsumval3  19817  mdetunilem8  22532  ordtrest2lem  23116  ptpjpre1  23484  fbfinnfr  23754  filufint  23833  ptcmplem2  23966  cphsqrtcl3  25112  ovoliun  25431  voliunlem3  25478  volsup  25482  cxpsqrt  26637  amgm  26926  wilthlem2  27004  sqff1o  27117  chtublem  27147  bposlem1  27220  bposlem3  27222  ostth  27575  nosupbnd1lem1  27645  noinfbnd1lem1  27660  cutlt  27874  clwwisshclwwslemlem  29988  atdmd  32373  atmd2  32375  mdsymlem4  32381  ordtrest2NEWlem  33930  eulerpartlemb  34376  dvelimalcased  35082  dvelimexcased  35084  fineqvac  35127  fineqvnttrclselem1  35129  dfon2lem9  35824  nn0prpwlem  36355  bj-ismooredr2  37143  ltflcei  37647  poimirlem30  37689  lplnexllnN  39602  2llnjaN  39604  paddasslem14  39871  cdleme32le  40485  dgrsub2  43167  naddgeoa  43426  evenwodadd  46915  iccelpart  47463  lighneallem3  47637  lighneal  47641