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  5296  onnseq  8275  oeeulem  8528  disjen  9063  cantnflem1  9599  ssfin4  10221  fin1a2lem12  10322  fin1a2lem13  10323  canthnumlem  10560  canthwelem  10562  supaddc  12112  supmul1  12114  ixxdisj  13302  ixxub  13308  ixxlb  13309  icodisj  13418  discr1  14190  01sqrexlem7  15199  bitsfzolem  16392  bitsfzo  16393  sqnprm  16661  mreexexlem2d  17600  acsinfd  18511  simpgntrivd  20064  prmgrpsimpgd  20080  ablsimpgprmd  20081  ornglmullt  20835  orngrmullt  20836  lbsextlem3  21148  lbsextlem4  21149  iunconn  23402  dissnlocfin  23503  ptcmplem4  24029  iccntr  24796  evth  24935  bcthlem5  25304  ovolicopnf  25500  vitalilem4  25587  dvferm1  25961  dvferm2  25963  dgreq0  26242  radcnvle  26400  isosctrlem2  26800  dmlogdmgm  27005  mersenne  27209  2sqn0  27416  pntlem3  27591  ostth2lem1  27600  tgbtwnne  28577  tglowdim1i  28588  tgbtwndiff  28593  tgbtwnconn1lem3  28661  legso  28686  tglineintmo  28729  tglineneq  28731  tglowdim2ln  28738  mirne  28754  mirhl  28766  krippenlem  28777  midexlem  28779  footexALT  28805  footexlem2  28807  colperpexlem3  28819  mideulem2  28821  opphllem  28822  oppnid  28833  opphllem2  28835  outpasch  28842  hlpasch  28843  hpgerlem  28852  colhp  28857  trgcopy  28891  tgasa1  28945  umgrnloop2  29234  ex-natded5.5  30500  ex-natded5.8  30503  ex-natded5.13  30505  unidifsnne  32626  ifnefals  32638  rexmul2  32847  hashpss  32902  nn0min  32914  ccatws1f1o  33031  elrgspnlem2  33324  fracfld  33389  0nellinds  33450  pidlnz  33456  drngidl  33513  drngidlhash  33514  0ringprmidl  33529  qsidomlem1  33532  mxidlirredi  33551  krull  33559  qsdrngi  33575  qsdrng  33577  rsprprmprmidlb  33603  rprmasso2  33606  1arithidom  33617  pidufd  33623  1arithufdlem3  33626  dfufd2  33630  0ringmon1p  33637  ig1pnunit  33681  mplmulmvr  33703  evlextv  33706  esplyfv  33734  esplyfval1  33737  esplyind  33739  vietadeg1  33742  exsslsb  33761  lvecdim0  33771  lindsunlem  33789  assafld  33802  fldextrspundgdvdslem  33845  extdgfialglem1  33857  irredminply  33881  constrextdg2lem  33913  constrext2chnlem  33915  2sqr3nconstr  33946  cos9thpinconstrlem2  33955  zarcls1  34034  zarclsint  34037  qqhre  34185  esumcvgre  34256  carsgclctunlem2  34484  oddpwdc  34519  eulerpartlemf  34535  ballotlemfc0  34658  ballotlemfcc  34659  ballotlemimin  34671  ballotlem1c  34673  reprinfz1  34787  bnj1417  35204  ttcwf2  36728  unbdqndv2lem2  36783  knoppndvlem13  36797  irrdiff  37653  topdifinffinlem  37674  pibt2  37744  poimirlem11  37963  poimirlem12  37964  aks4d1p7  42533  aks4d1p8d2  42535  aks4d1p8  42537  aks4d1p9  42538  fldhmf1  42540  hashscontpow1  42571  aks6d1c5  42589  imo72b2  44614  iunconnlem2  45376  n0p  45491  uzwo4  45499  ssnct  45523  nsstr  45540  disjrnmpt2  45633  difmap  45651  difmapsn  45656  mapssbi  45657  xrlexaddrp  45797  infleinflem2  45815  xrralrecnnge  45834  supminfxr2  45912  xrpnf  45928  icoub  45971  ioonct  45982  ressioosup  46000  ressiooinf  46002  limclner  46094  limsupub  46147  climxrrelem  46192  climlimsupcex  46212  icccncfext  46330  fperdvper  46362  dvdivbd  46366  dvdsn1add  46382  dvmptfprodlem  46387  dvnprodlem3  46391  fourierdlem10  46560  fourierdlem19  46569  fourierdlem20  46570  fourierdlem35  46585  fourierdlem40  46590  fourierdlem41  46591  fourierdlem42  46592  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem57  46606  fourierdlem58  46607  fourierdlem59  46608  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem68  46617  fourierdlem74  46623  fourierdlem75  46624  fourierdlem78  46627  fourierdlem79  46628  fourierdlem80  46629  elaa2  46677  etransclem35  46712  etransclem38  46715  fge0npnf  46810  sge0tsms  46823  sge0rern  46831  sge0supre  46832  sge0le  46850  sge0fodjrnlem  46859  sge0rpcpnf  46864  meadjun  46905  meadjiunlem  46908  hoidmvlelem2  47039  hspdifhsp  47059  ovolval4lem1  47092