Theorem pm2.65da 817

Description: Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)

Hypotheses

Ref	Expression
pm2.65da.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.65da.2	⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)

Assertion

Ref	Expression
pm2.65da	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.65da

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 412	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 196	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  condan  818  nelrdva  3711  eqsnuniex  5361  onnseq  8384  oeeulem  8639  disjen  9174  cantnflem1  9729  ssfin4  10350  fin1a2lem12  10451  fin1a2lem13  10452  canthnumlem  10688  canthwelem  10690  supaddc  12235  supmul1  12237  ixxdisj  13402  ixxub  13408  ixxlb  13409  icodisj  13516  discr1  14278  01sqrexlem7  15287  bitsfzolem  16471  bitsfzo  16472  sqnprm  16739  mreexexlem2d  17688  acsinfd  18601  simpgntrivd  20118  prmgrpsimpgd  20134  ablsimpgprmd  20135  lbsextlem3  21162  lbsextlem4  21163  iunconn  23436  dissnlocfin  23537  ptcmplem4  24063  iccntr  24843  evth  24991  bcthlem5  25362  ovolicopnf  25559  vitalilem4  25646  dvferm1  26023  dvferm2  26025  dgreq0  26305  radcnvle  26463  isosctrlem2  26862  dmlogdmgm  27067  mersenne  27271  2sqn0  27478  pntlem3  27653  ostth2lem1  27662  tgbtwnne  28498  tglowdim1i  28509  tgbtwndiff  28514  tgbtwnconn1lem3  28582  legso  28607  tglineintmo  28650  tglineneq  28652  tglowdim2ln  28659  mirne  28675  mirhl  28687  krippenlem  28698  midexlem  28700  footexALT  28726  footexlem2  28728  colperpexlem3  28740  mideulem2  28742  opphllem  28743  oppnid  28754  opphllem2  28756  outpasch  28763  hlpasch  28764  hpgerlem  28773  colhp  28778  trgcopy  28812  tgasa1  28866  umgrnloop2  29163  ex-natded5.5  30429  ex-natded5.8  30432  ex-natded5.13  30434  unidifsnne  32554  ifnefals  32561  hashpss  32813  nn0min  32822  ccatws1f1o  32936  elrgspnlem2  33247  fracfld  33310  ornglmullt  33337  orngrmullt  33338  0nellinds  33398  pidlnz  33404  drngidl  33461  drngidlhash  33462  0ringprmidl  33477  qsidomlem1  33480  mxidlirredi  33499  krull  33507  qsdrngi  33523  qsdrng  33525  rsprprmprmidlb  33551  rprmasso2  33554  1arithidom  33565  pidufd  33571  1arithufdlem3  33574  dfufd2  33578  0ringmon1p  33583  ig1pnunit  33621  exsslsb  33647  lvecdim0  33657  lindsunlem  33675  assafld  33688  fldextrspundgdvdslem  33730  irredminply  33757  constrextdg2lem  33789  zarcls1  33868  zarclsint  33871  qqhre  34021  esumcvgre  34092  carsgclctunlem2  34321  oddpwdc  34356  eulerpartlemf  34372  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemimin  34508  ballotlem1c  34510  reprinfz1  34637  bnj1417  35055  unbdqndv2lem2  36511  knoppndvlem13  36525  irrdiff  37327  topdifinffinlem  37348  pibt2  37418  poimirlem11  37638  poimirlem12  37639  aks4d1p7  42084  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1p9  42089  fldhmf1  42091  hashscontpow1  42122  aks6d1c5  42140  imo72b2  44185  iunconnlem2  44955  n0p  45050  uzwo4  45058  ssnct  45082  nsstr  45100  disjrnmpt2  45193  difmap  45212  difmapsn  45217  mapssbi  45218  xrlexaddrp  45363  infleinflem2  45382  xrralrecnnge  45401  supminfxr2  45480  xrpnf  45496  icoub  45539  ioonct  45550  ressioosup  45568  ressiooinf  45570  limclner  45666  limsupub  45719  climxrrelem  45764  climlimsupcex  45784  icccncfext  45902  fperdvper  45934  dvdivbd  45938  dvdsn1add  45954  dvmptfprodlem  45959  dvnprodlem3  45963  fourierdlem10  46132  fourierdlem19  46141  fourierdlem20  46142  fourierdlem35  46157  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem68  46189  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem79  46200  fourierdlem80  46201  elaa2  46249  etransclem35  46284  etransclem38  46287  fge0npnf  46382  sge0tsms  46395  sge0rern  46403  sge0supre  46404  sge0le  46422  sge0fodjrnlem  46431  sge0rpcpnf  46436  meadjun  46477  meadjiunlem  46480  hoidmvlelem2  46611  hspdifhsp  46631  ovolval4lem1  46664