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  3652  eqsnuniex  5304  onnseq  8284  oeeulem  8537  disjen  9072  cantnflem1  9610  ssfin4  10232  fin1a2lem12  10333  fin1a2lem13  10334  canthnumlem  10571  canthwelem  10573  supaddc  12123  supmul1  12125  ixxdisj  13313  ixxub  13319  ixxlb  13320  icodisj  13429  discr1  14201  01sqrexlem7  15210  bitsfzolem  16403  bitsfzo  16404  sqnprm  16672  mreexexlem2d  17611  acsinfd  18522  simpgntrivd  20075  prmgrpsimpgd  20091  ablsimpgprmd  20092  ornglmullt  20846  orngrmullt  20847  lbsextlem3  21158  lbsextlem4  21159  iunconn  23393  dissnlocfin  23494  ptcmplem4  24020  iccntr  24787  evth  24926  bcthlem5  25295  ovolicopnf  25491  vitalilem4  25578  dvferm1  25952  dvferm2  25954  dgreq0  26230  radcnvle  26385  isosctrlem2  26783  dmlogdmgm  26987  mersenne  27190  2sqn0  27397  pntlem3  27572  ostth2lem1  27581  tgbtwnne  28558  tglowdim1i  28569  tgbtwndiff  28574  tgbtwnconn1lem3  28642  legso  28667  tglineintmo  28710  tglineneq  28712  tglowdim2ln  28719  mirne  28735  mirhl  28747  krippenlem  28758  midexlem  28760  footexALT  28786  footexlem2  28788  colperpexlem3  28800  mideulem2  28802  opphllem  28803  oppnid  28814  opphllem2  28816  outpasch  28823  hlpasch  28824  hpgerlem  28833  colhp  28838  trgcopy  28872  tgasa1  28926  umgrnloop2  29215  ex-natded5.5  30480  ex-natded5.8  30483  ex-natded5.13  30485  unidifsnne  32606  ifnefals  32618  rexmul2  32827  hashpss  32882  nn0min  32894  ccatws1f1o  33011  elrgspnlem2  33304  fracfld  33369  0nellinds  33430  pidlnz  33436  drngidl  33493  drngidlhash  33494  0ringprmidl  33509  qsidomlem1  33512  mxidlirredi  33531  krull  33539  qsdrngi  33555  qsdrng  33557  rsprprmprmidlb  33583  rprmasso2  33586  1arithidom  33597  pidufd  33603  1arithufdlem3  33606  dfufd2  33610  0ringmon1p  33617  ig1pnunit  33661  mplmulmvr  33683  evlextv  33686  esplyfv  33714  esplyfval1  33717  esplyind  33719  vietadeg1  33722  exsslsb  33741  lvecdim0  33751  lindsunlem  33768  assafld  33781  fldextrspundgdvdslem  33824  extdgfialglem1  33836  irredminply  33860  constrextdg2lem  33892  constrext2chnlem  33894  2sqr3nconstr  33925  cos9thpinconstrlem2  33934  zarcls1  34013  zarclsint  34016  qqhre  34164  esumcvgre  34235  carsgclctunlem2  34463  oddpwdc  34498  eulerpartlemf  34514  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemimin  34650  ballotlem1c  34652  reprinfz1  34766  bnj1417  35183  ttcwf2  36707  unbdqndv2lem2  36770  knoppndvlem13  36784  irrdiff  37640  topdifinffinlem  37663  pibt2  37733  poimirlem11  37952  poimirlem12  37953  aks4d1p7  42522  aks4d1p8d2  42524  aks4d1p8  42526  aks4d1p9  42527  fldhmf1  42529  hashscontpow1  42560  aks6d1c5  42578  imo72b2  44599  iunconnlem2  45361  n0p  45476  uzwo4  45484  ssnct  45508  nsstr  45525  disjrnmpt2  45618  difmap  45636  difmapsn  45641  mapssbi  45642  xrlexaddrp  45782  infleinflem2  45800  xrralrecnnge  45819  supminfxr2  45897  xrpnf  45913  icoub  45956  ioonct  45967  ressioosup  45985  ressiooinf  45987  limclner  46079  limsupub  46132  climxrrelem  46177  climlimsupcex  46197  icccncfext  46315  fperdvper  46347  dvdivbd  46351  dvdsn1add  46367  dvmptfprodlem  46372  dvnprodlem3  46376  fourierdlem10  46545  fourierdlem19  46554  fourierdlem20  46555  fourierdlem35  46570  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem68  46602  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem80  46614  elaa2  46662  etransclem35  46697  etransclem38  46700  fge0npnf  46795  sge0tsms  46808  sge0rern  46816  sge0supre  46817  sge0le  46835  sge0fodjrnlem  46844  sge0rpcpnf  46849  meadjun  46890  meadjiunlem  46893  hoidmvlelem2  47024  hspdifhsp  47044  ovolval4lem1  47077