Theorem pm2.65da 815

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

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

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 206  df-an 397

This theorem is referenced by:  condan  816  nelrdva  3701  eqsnuniex  5359  onnseq  8343  oeeulem  8600  disjen  9133  cantnflem1  9683  ssfin4  10304  fin1a2lem12  10405  fin1a2lem13  10406  canthnumlem  10642  canthwelem  10644  supaddc  12180  supmul1  12182  ixxdisj  13338  ixxub  13344  ixxlb  13345  icodisj  13452  discr1  14201  01sqrexlem7  15194  bitsfzolem  16374  bitsfzo  16375  sqnprm  16638  mreexexlem2d  17588  acsinfd  18508  simpgntrivd  19967  prmgrpsimpgd  19983  ablsimpgprmd  19984  lbsextlem3  20772  lbsextlem4  20773  iunconn  22931  dissnlocfin  23032  ptcmplem4  23558  iccntr  24336  evth  24474  bcthlem5  24844  ovolicopnf  25040  vitalilem4  25127  dvferm1  25501  dvferm2  25503  dgreq0  25778  radcnvle  25931  isosctrlem2  26321  dmlogdmgm  26525  mersenne  26727  2sqn0  26934  pntlem3  27109  ostth2lem1  27118  tgbtwnne  27738  tglowdim1i  27749  tgbtwndiff  27754  tgbtwnconn1lem3  27822  legso  27847  tglineintmo  27890  tglineneq  27892  tglowdim2ln  27899  mirne  27915  mirhl  27927  krippenlem  27938  midexlem  27940  footexALT  27966  footexlem2  27968  colperpexlem3  27980  mideulem2  27982  opphllem  27983  oppnid  27994  opphllem2  27996  outpasch  28003  hlpasch  28004  hpgerlem  28013  colhp  28018  trgcopy  28052  tgasa1  28106  umgrnloop2  28403  ex-natded5.5  29660  ex-natded5.8  29663  ex-natded5.13  29665  unidifsnne  31768  ifnefals  31775  nn0min  32021  ornglmullt  32420  orngrmullt  32421  0nellinds  32478  pidlnz  32483  drngidl  32546  drngidlhash  32547  0ringprmidl  32563  qsidomlem1  32566  mxidlirredi  32582  krull  32589  qsdrngi  32604  qsdrng  32606  0ringmon1p  32631  ig1pnunit  32665  lvecdim0  32686  lindsunlem  32704  zarcls1  32844  zarclsint  32847  qqhre  32995  esumcvgre  33084  carsgclctunlem2  33313  oddpwdc  33348  eulerpartlemf  33364  ballotlemfc0  33486  ballotlemfcc  33487  ballotlemimin  33499  ballotlem1c  33501  reprinfz1  33629  bnj1417  34047  unbdqndv2lem2  35381  knoppndvlem13  35395  irrdiff  36202  topdifinffinlem  36223  pibt2  36293  poimirlem11  36494  poimirlem12  36495  aks4d1p7  40943  aks4d1p8d2  40945  aks4d1p8  40947  aks4d1p9  40948  fldhmf1  40950  imo72b2  42914  iunconnlem2  43686  n0p  43720  uzwo4  43730  ssnct  43756  nsstr  43774  disjrnmpt2  43876  difmap  43896  difmapsn  43901  mapssbi  43902  xrlexaddrp  44052  infleinflem2  44071  xrralrecnnge  44090  supminfxr2  44169  xrpnf  44186  icoub  44229  ioonct  44240  ressioosup  44258  ressiooinf  44260  limclner  44357  limsupub  44410  climxrrelem  44455  climlimsupcex  44475  icccncfext  44593  fperdvper  44625  dvdivbd  44629  dvdsn1add  44645  dvmptfprodlem  44650  dvnprodlem3  44654  fourierdlem10  44823  fourierdlem19  44832  fourierdlem20  44833  fourierdlem35  44848  fourierdlem40  44853  fourierdlem41  44854  fourierdlem42  44855  fourierdlem46  44858  fourierdlem48  44860  fourierdlem49  44861  fourierdlem57  44869  fourierdlem58  44870  fourierdlem59  44871  fourierdlem63  44875  fourierdlem64  44876  fourierdlem65  44877  fourierdlem68  44880  fourierdlem74  44886  fourierdlem75  44887  fourierdlem78  44890  fourierdlem79  44891  fourierdlem80  44892  elaa2  44940  etransclem35  44975  etransclem38  44978  fge0npnf  45073  sge0tsms  45086  sge0rern  45094  sge0supre  45095  sge0le  45113  sge0fodjrnlem  45122  sge0rpcpnf  45127  meadjun  45168  meadjiunlem  45171  hoidmvlelem2  45302  hspdifhsp  45322  ovolval4lem1  45355