Theorem pm2.65da 813

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

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

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 395

This theorem is referenced by:  condan  814  nelrdva  3700  eqsnuniex  5358  onnseq  8346  oeeulem  8603  disjen  9136  cantnflem1  9686  ssfin4  10307  fin1a2lem12  10408  fin1a2lem13  10409  canthnumlem  10645  canthwelem  10647  supaddc  12185  supmul1  12187  ixxdisj  13343  ixxub  13349  ixxlb  13350  icodisj  13457  discr1  14206  01sqrexlem7  15199  bitsfzolem  16379  bitsfzo  16380  sqnprm  16643  mreexexlem2d  17593  acsinfd  18513  simpgntrivd  20009  prmgrpsimpgd  20025  ablsimpgprmd  20026  lbsextlem3  20918  lbsextlem4  20919  iunconn  23152  dissnlocfin  23253  ptcmplem4  23779  iccntr  24557  evth  24705  bcthlem5  25076  ovolicopnf  25273  vitalilem4  25360  dvferm1  25737  dvferm2  25739  dgreq0  26015  radcnvle  26168  isosctrlem2  26560  dmlogdmgm  26764  mersenne  26966  2sqn0  27173  pntlem3  27348  ostth2lem1  27357  tgbtwnne  28008  tglowdim1i  28019  tgbtwndiff  28024  tgbtwnconn1lem3  28092  legso  28117  tglineintmo  28160  tglineneq  28162  tglowdim2ln  28169  mirne  28185  mirhl  28197  krippenlem  28208  midexlem  28210  footexALT  28236  footexlem2  28238  colperpexlem3  28250  mideulem2  28252  opphllem  28253  oppnid  28264  opphllem2  28266  outpasch  28273  hlpasch  28274  hpgerlem  28283  colhp  28288  trgcopy  28322  tgasa1  28376  umgrnloop2  28673  ex-natded5.5  29930  ex-natded5.8  29933  ex-natded5.13  29935  unidifsnne  32040  ifnefals  32047  nn0min  32293  ornglmullt  32695  orngrmullt  32696  0nellinds  32757  pidlnz  32762  drngidl  32825  drngidlhash  32826  0ringprmidl  32842  qsidomlem1  32845  mxidlirredi  32861  krull  32868  qsdrngi  32883  qsdrng  32885  0ringmon1p  32910  ig1pnunit  32946  lvecdim0  32979  lindsunlem  32997  zarcls1  33147  zarclsint  33150  qqhre  33298  esumcvgre  33387  carsgclctunlem2  33616  oddpwdc  33651  eulerpartlemf  33667  ballotlemfc0  33789  ballotlemfcc  33790  ballotlemimin  33802  ballotlem1c  33804  reprinfz1  33932  bnj1417  34350  unbdqndv2lem2  35689  knoppndvlem13  35703  irrdiff  36510  topdifinffinlem  36531  pibt2  36601  poimirlem11  36802  poimirlem12  36803  aks4d1p7  41254  aks4d1p8d2  41256  aks4d1p8  41258  aks4d1p9  41259  fldhmf1  41261  imo72b2  43226  iunconnlem2  43998  n0p  44031  uzwo4  44041  ssnct  44067  nsstr  44085  disjrnmpt2  44185  difmap  44204  difmapsn  44209  mapssbi  44210  xrlexaddrp  44360  infleinflem2  44379  xrralrecnnge  44398  supminfxr2  44477  xrpnf  44494  icoub  44537  ioonct  44548  ressioosup  44566  ressiooinf  44568  limclner  44665  limsupub  44718  climxrrelem  44763  climlimsupcex  44783  icccncfext  44901  fperdvper  44933  dvdivbd  44937  dvdsn1add  44953  dvmptfprodlem  44958  dvnprodlem3  44962  fourierdlem10  45131  fourierdlem19  45140  fourierdlem20  45141  fourierdlem35  45156  fourierdlem40  45161  fourierdlem41  45162  fourierdlem42  45163  fourierdlem46  45166  fourierdlem48  45168  fourierdlem49  45169  fourierdlem57  45177  fourierdlem58  45178  fourierdlem59  45179  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem68  45188  fourierdlem74  45194  fourierdlem75  45195  fourierdlem78  45198  fourierdlem79  45199  fourierdlem80  45200  elaa2  45248  etransclem35  45283  etransclem38  45286  fge0npnf  45381  sge0tsms  45394  sge0rern  45402  sge0supre  45403  sge0le  45421  sge0fodjrnlem  45430  sge0rpcpnf  45435  meadjun  45476  meadjiunlem  45479  hoidmvlelem2  45610  hspdifhsp  45630  ovolval4lem1  45663