Theorem pm2.65da 828

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 417	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 417	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 199	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 210  df-an 401

This theorem is referenced by:  condan  829  nelrdva  3675  eqsnuniex  5333  onnseq  8331  oeeulem  8587  disjen  9122  cantnflem1  9658  ssfin4  10294  fin1a2lem12  10395  fin1a2lem13  10396  canthnumlem  10633  canthwelem  10635  supaddc  12182  supmul1  12184  ixxdisj  13387  ixxub  13393  ixxlb  13394  icodisj  13503  discr1  14275  hashpss  14446  01sqrexlem7  15299  bitsfzolem  16492  bitsfzo  16493  sqnprm  16761  mreexexlem2d  17701  acsinfd  18612  simpgntrivd  20170  prmgrpsimpgd  20186  ablsimpgprmd  20187  ornglmullt  20950  orngrmullt  20951  lbsextlem3  21262  lbsextlem4  21263  0ringprmidl  21446  qsidomlem1  21449  iunconn  23554  dissnlocfin  23655  ptcmplem4  24181  iccntr  24948  evth  25087  bcthlem5  25456  ovolicopnf  25652  vitalilem4  25739  dvferm1  26113  dvferm2  26115  dgreq0  26391  radcnvle  26549  isosctrlem2  26950  dmlogdmgm  27154  mersenne  27357  2sqn0  27564  pntlem3  27739  ostth2lem1  27748  tgbtwnne  28725  tglowdim1i  28736  tgbtwndiff  28741  tgbtwnconn1lem3  28809  legso  28834  tglineintmo  28877  tglineneq  28880  tglowdim2ln  28887  tglnpt4  28890  mirne  28906  mirhl  28918  krippenlem  28929  midexlem  28931  footexALT  28957  footexlem2  28959  colperpexlem3  28972  mideulem2  28974  opphllem  28975  oppnid  28986  opphllem2  28988  outpasch  28996  hlpasch  28997  hpgerlem  29006  colhp  29011  trgcopy  29072  tgasa1  29130  prlnghpg  29151  prlngmolem1  29155  prlngmolem2  29156  umgrnloop2  29437  ex-natded5.5  30702  ex-natded5.8  30705  ex-natded5.13  30707  unidifsnne  32823  ifnefals  32835  rexmul2  33040  nn0min  33106  ccatws1f1o  33212  elrgspnlem2  33504  fracfld  33572  0nellinds  33628  pidlnz  33633  drngidl  33685  drngidlhash  33686  mxidlirredi  33699  krull  33706  qsdrngi  33722  qsdrng  33724  rsprprmprmidlb  33758  rprmasso2  33761  1arithidom  33772  pidufd  33778  1arithufdlem3  33781  dfufd2  33785  0ringmon1p  33792  ig1pnunit  33836  mplmulmvr  33874  evlextv  33877  esplyfv  33905  esplyfval1  33908  esplyind  33910  vietadeg1  33913  exsslsb  33932  lvecdim0  33942  lindsunlem  33959  assafld  33972  fldextrspundgdvdslem  34015  extdgfialglem1  34027  irredminply  34051  constrextdg2lem  34083  constrext2chnlem  34085  2sqr3nconstr  34116  cos9thpinconstrlem2  34125  zarcls1  34204  zarclsint  34207  qqhre  34355  esumcvgre  34426  carsgclctunlem2  34654  oddpwdc  34689  eulerpartlemf  34705  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemimin  34841  ballotlem1c  34843  reprinfz1  34954  bnj1417  35374  ttcwf2  36959  unbdqndv2lem2  37022  knoppndvlem13  37036  irrdiff  37893  topdifinffinlem  37916  pibt2  37986  poimirlem11  38205  poimirlem12  38206  aks4d1p7  42775  aks4d1p8d2  42777  aks4d1p8  42779  aks4d1p9  42780  fldhmf1  42782  hashscontpow1  42813  aks6d1c5  42831  imo72b2  44825  iunconnlem2  45570  n0p  45692  uzwo4  45700  ssnct  45724  nsstr  45740  disjrnmpt2  45833  difmap  45850  difmapsn  45855  mapssbi  45856  xrlexaddrp  45995  infleinflem2  46013  xrralrecnnge  46032  supminfxr2  46110  xrpnf  46126  icoub  46169  ioonct  46180  ressioosup  46198  ressiooinf  46200  limclner  46292  limsupub  46345  climxrrelem  46390  climlimsupcex  46410  icccncfext  46528  fperdvper  46560  dvdivbd  46564  dvdsn1add  46580  dvmptfprodlem  46585  dvnprodlem3  46589  fourierdlem10  46758  fourierdlem19  46767  fourierdlem20  46768  fourierdlem35  46783  fourierdlem40  46788  fourierdlem41  46789  fourierdlem42  46790  fourierdlem46  46793  fourierdlem48  46795  fourierdlem49  46796  fourierdlem57  46804  fourierdlem58  46805  fourierdlem59  46806  fourierdlem63  46810  fourierdlem64  46811  fourierdlem65  46812  fourierdlem68  46815  fourierdlem74  46821  fourierdlem75  46822  fourierdlem78  46825  fourierdlem79  46826  fourierdlem80  46827  elaa2  46875  etransclem35  46910  etransclem38  46913  fge0npnf  47008  sge0tsms  47021  sge0rern  47029  sge0supre  47030  sge0le  47048  sge0fodjrnlem  47057  sge0rpcpnf  47062  meadjun  47103  meadjiunlem  47106  hoidmvlelem2  47237  hspdifhsp  47257  ovolval4lem1  47290