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  3667  eqsnuniex  5303  onnseq  8274  oeeulem  8526  disjen  9058  cantnflem1  9604  ssfin4  10223  fin1a2lem12  10324  fin1a2lem13  10325  canthnumlem  10561  canthwelem  10563  supaddc  12110  supmul1  12112  ixxdisj  13281  ixxub  13287  ixxlb  13288  icodisj  13397  discr1  14164  01sqrexlem7  15173  bitsfzolem  16363  bitsfzo  16364  sqnprm  16631  mreexexlem2d  17569  acsinfd  18480  simpgntrivd  19997  prmgrpsimpgd  20013  ablsimpgprmd  20014  ornglmullt  20772  orngrmullt  20773  lbsextlem3  21085  lbsextlem4  21086  iunconn  23331  dissnlocfin  23432  ptcmplem4  23958  iccntr  24726  evth  24874  bcthlem5  25244  ovolicopnf  25441  vitalilem4  25528  dvferm1  25905  dvferm2  25907  dgreq0  26187  radcnvle  26345  isosctrlem2  26745  dmlogdmgm  26950  mersenne  27154  2sqn0  27361  pntlem3  27536  ostth2lem1  27545  tgbtwnne  28453  tglowdim1i  28464  tgbtwndiff  28469  tgbtwnconn1lem3  28537  legso  28562  tglineintmo  28605  tglineneq  28607  tglowdim2ln  28614  mirne  28630  mirhl  28642  krippenlem  28653  midexlem  28655  footexALT  28681  footexlem2  28683  colperpexlem3  28695  mideulem2  28697  opphllem  28698  oppnid  28709  opphllem2  28711  outpasch  28718  hlpasch  28719  hpgerlem  28728  colhp  28733  trgcopy  28767  tgasa1  28821  umgrnloop2  29109  ex-natded5.5  30372  ex-natded5.8  30375  ex-natded5.13  30377  unidifsnne  32498  ifnefals  32510  rexmul2  32710  hashpss  32767  nn0min  32778  ccatws1f1o  32906  elrgspnlem2  33193  fracfld  33257  0nellinds  33317  pidlnz  33323  drngidl  33380  drngidlhash  33381  0ringprmidl  33396  qsidomlem1  33399  mxidlirredi  33418  krull  33426  qsdrngi  33442  qsdrng  33444  rsprprmprmidlb  33470  rprmasso2  33473  1arithidom  33484  pidufd  33490  1arithufdlem3  33493  dfufd2  33497  0ringmon1p  33502  ig1pnunit  33542  exsslsb  33568  lvecdim0  33578  lindsunlem  33596  assafld  33609  fldextrspundgdvdslem  33651  irredminply  33682  constrextdg2lem  33714  constrext2chnlem  33716  2sqr3nconstr  33747  cos9thpinconstrlem2  33756  zarcls1  33835  zarclsint  33838  qqhre  33986  esumcvgre  34057  carsgclctunlem2  34286  oddpwdc  34321  eulerpartlemf  34337  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemimin  34473  ballotlem1c  34475  reprinfz1  34589  bnj1417  35007  unbdqndv2lem2  36483  knoppndvlem13  36497  irrdiff  37299  topdifinffinlem  37320  pibt2  37390  poimirlem11  37610  poimirlem12  37611  aks4d1p7  42056  aks4d1p8d2  42058  aks4d1p8  42060  aks4d1p9  42061  fldhmf1  42063  hashscontpow1  42094  aks6d1c5  42112  imo72b2  44145  iunconnlem2  44908  n0p  45023  uzwo4  45031  ssnct  45055  nsstr  45073  disjrnmpt2  45166  difmap  45185  difmapsn  45190  mapssbi  45191  xrlexaddrp  45332  infleinflem2  45351  xrralrecnnge  45370  supminfxr2  45449  xrpnf  45465  icoub  45508  ioonct  45519  ressioosup  45537  ressiooinf  45539  limclner  45633  limsupub  45686  climxrrelem  45731  climlimsupcex  45751  icccncfext  45869  fperdvper  45901  dvdivbd  45905  dvdsn1add  45921  dvmptfprodlem  45926  dvnprodlem3  45930  fourierdlem10  46099  fourierdlem19  46108  fourierdlem20  46109  fourierdlem35  46124  fourierdlem40  46129  fourierdlem41  46130  fourierdlem42  46131  fourierdlem46  46134  fourierdlem48  46136  fourierdlem49  46137  fourierdlem57  46145  fourierdlem58  46146  fourierdlem59  46147  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem68  46156  fourierdlem74  46162  fourierdlem75  46163  fourierdlem78  46166  fourierdlem79  46167  fourierdlem80  46168  elaa2  46216  etransclem35  46251  etransclem38  46254  fge0npnf  46349  sge0tsms  46362  sge0rern  46370  sge0supre  46371  sge0le  46389  sge0fodjrnlem  46398  sge0rpcpnf  46403  meadjun  46444  meadjiunlem  46447  hoidmvlelem2  46578  hspdifhsp  46598  ovolval4lem1  46631