Theorem pm2.65da 816

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  817  nelrdva  3661  eqsnuniex  5303  onnseq  8273  oeeulem  8525  disjen  9057  cantnflem1  9589  ssfin4  10211  fin1a2lem12  10312  fin1a2lem13  10313  canthnumlem  10549  canthwelem  10551  supaddc  12099  supmul1  12101  ixxdisj  13270  ixxub  13276  ixxlb  13277  icodisj  13386  discr1  14156  01sqrexlem7  15165  bitsfzolem  16355  bitsfzo  16356  sqnprm  16623  mreexexlem2d  17561  acsinfd  18472  simpgntrivd  20022  prmgrpsimpgd  20038  ablsimpgprmd  20039  ornglmullt  20794  orngrmullt  20795  lbsextlem3  21107  lbsextlem4  21108  iunconn  23353  dissnlocfin  23454  ptcmplem4  23980  iccntr  24747  evth  24895  bcthlem5  25265  ovolicopnf  25462  vitalilem4  25549  dvferm1  25926  dvferm2  25928  dgreq0  26208  radcnvle  26366  isosctrlem2  26766  dmlogdmgm  26971  mersenne  27175  2sqn0  27382  pntlem3  27557  ostth2lem1  27566  tgbtwnne  28478  tglowdim1i  28489  tgbtwndiff  28494  tgbtwnconn1lem3  28562  legso  28587  tglineintmo  28630  tglineneq  28632  tglowdim2ln  28639  mirne  28655  mirhl  28667  krippenlem  28678  midexlem  28680  footexALT  28706  footexlem2  28708  colperpexlem3  28720  mideulem2  28722  opphllem  28723  oppnid  28734  opphllem2  28736  outpasch  28743  hlpasch  28744  hpgerlem  28753  colhp  28758  trgcopy  28792  tgasa1  28846  umgrnloop2  29135  ex-natded5.5  30401  ex-natded5.8  30404  ex-natded5.13  30406  unidifsnne  32527  ifnefals  32539  rexmul2  32748  hashpss  32802  nn0min  32814  ccatws1f1o  32943  elrgspnlem2  33221  fracfld  33285  0nellinds  33346  pidlnz  33352  drngidl  33409  drngidlhash  33410  0ringprmidl  33425  qsidomlem1  33428  mxidlirredi  33447  krull  33455  qsdrngi  33471  qsdrng  33473  rsprprmprmidlb  33499  rprmasso2  33502  1arithidom  33513  pidufd  33519  1arithufdlem3  33522  dfufd2  33526  0ringmon1p  33531  ig1pnunit  33572  esplyfv  33602  exsslsb  33620  lvecdim0  33630  lindsunlem  33648  assafld  33661  fldextrspundgdvdslem  33704  extdgfialglem1  33716  irredminply  33740  constrextdg2lem  33772  constrext2chnlem  33774  2sqr3nconstr  33805  cos9thpinconstrlem2  33814  zarcls1  33893  zarclsint  33896  qqhre  34044  esumcvgre  34115  carsgclctunlem2  34343  oddpwdc  34378  eulerpartlemf  34394  ballotlemfc0  34517  ballotlemfcc  34518  ballotlemimin  34530  ballotlem1c  34532  reprinfz1  34646  bnj1417  35064  unbdqndv2lem2  36565  knoppndvlem13  36579  irrdiff  37381  topdifinffinlem  37402  pibt2  37472  poimirlem11  37681  poimirlem12  37682  aks4d1p7  42186  aks4d1p8d2  42188  aks4d1p8  42190  aks4d1p9  42191  fldhmf1  42193  hashscontpow1  42224  aks6d1c5  42242  imo72b2  44279  iunconnlem2  45041  n0p  45156  uzwo4  45164  ssnct  45188  nsstr  45206  disjrnmpt2  45299  difmap  45318  difmapsn  45323  mapssbi  45324  xrlexaddrp  45465  infleinflem2  45483  xrralrecnnge  45502  supminfxr2  45581  xrpnf  45597  icoub  45640  ioonct  45651  ressioosup  45669  ressiooinf  45671  limclner  45763  limsupub  45816  climxrrelem  45861  climlimsupcex  45881  icccncfext  45999  fperdvper  46031  dvdivbd  46035  dvdsn1add  46051  dvmptfprodlem  46056  dvnprodlem3  46060  fourierdlem10  46229  fourierdlem19  46238  fourierdlem20  46239  fourierdlem35  46254  fourierdlem40  46259  fourierdlem41  46260  fourierdlem42  46261  fourierdlem46  46264  fourierdlem48  46266  fourierdlem49  46267  fourierdlem57  46275  fourierdlem58  46276  fourierdlem59  46277  fourierdlem63  46281  fourierdlem64  46282  fourierdlem65  46283  fourierdlem68  46286  fourierdlem74  46292  fourierdlem75  46293  fourierdlem78  46296  fourierdlem79  46297  fourierdlem80  46298  elaa2  46346  etransclem35  46381  etransclem38  46384  fge0npnf  46479  sge0tsms  46492  sge0rern  46500  sge0supre  46501  sge0le  46519  sge0fodjrnlem  46528  sge0rpcpnf  46533  meadjun  46574  meadjiunlem  46577  hoidmvlelem2  46708  hspdifhsp  46728  ovolval4lem1  46761