Theorem pm2.65da 814

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  815  nelrdva  3641  eqsnuniex  5284  onnseq  8184  oeeulem  8441  disjen  8930  cantnflem1  9456  ssfin4  10075  fin1a2lem12  10176  fin1a2lem13  10177  canthnumlem  10413  canthwelem  10415  supaddc  11951  supmul1  11953  ixxdisj  13103  ixxub  13109  ixxlb  13110  icodisj  13217  discr1  13963  sqrlem7  14969  bitsfzolem  16150  bitsfzo  16151  sqnprm  16416  mreexexlem2d  17363  acsinfd  18283  simpgntrivd  19710  prmgrpsimpgd  19726  ablsimpgprmd  19727  lbsextlem3  20431  lbsextlem4  20432  iunconn  22588  dissnlocfin  22689  ptcmplem4  23215  iccntr  23993  evth  24131  bcthlem5  24501  ovolicopnf  24697  vitalilem4  24784  dvferm1  25158  dvferm2  25160  dgreq0  25435  radcnvle  25588  isosctrlem2  25978  dmlogdmgm  26182  mersenne  26384  2sqn0  26591  pntlem3  26766  ostth2lem1  26775  tgbtwnne  26860  tglowdim1i  26871  tgbtwndiff  26876  tgbtwnconn1lem3  26944  legso  26969  tglineintmo  27012  tglineneq  27014  tglowdim2ln  27021  mirne  27037  mirhl  27049  krippenlem  27060  midexlem  27062  footexALT  27088  footexlem2  27090  colperpexlem3  27102  mideulem2  27104  opphllem  27105  oppnid  27116  opphllem2  27118  outpasch  27125  hlpasch  27126  hpgerlem  27135  colhp  27140  trgcopy  27174  tgasa1  27228  umgrnloop2  27525  ex-natded5.5  28783  ex-natded5.8  28786  ex-natded5.13  28788  unidifsnne  30893  nn0min  31143  ornglmullt  31515  orngrmullt  31516  0nellinds  31575  pidlnz  31580  0ringprmidl  31634  qsidomlem1  31637  krull  31652  lvecdim0  31699  lindsunlem  31714  zarcls1  31828  zarclsint  31831  qqhre  31979  esumcvgre  32068  carsgclctunlem2  32295  oddpwdc  32330  eulerpartlemf  32346  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemimin  32481  ballotlem1c  32483  reprinfz1  32611  bnj1417  33030  unbdqndv2lem2  34699  knoppndvlem13  34713  irrdiff  35506  topdifinffinlem  35527  pibt2  35597  poimirlem11  35797  poimirlem12  35798  aks4d1p7  40098  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  imo72b2  41790  iunconnlem2  42562  n0p  42598  uzwo4  42608  ssnct  42634  nsstr  42652  disjrnmpt2  42733  difmap  42754  difmapsn  42759  mapssbi  42760  xrlexaddrp  42898  infleinflem2  42917  xrralrecnnge  42937  supminfxr2  43016  xrpnf  43033  icoub  43071  ioonct  43082  ressioosup  43100  ressiooinf  43102  limclner  43199  limsupub  43252  climxrrelem  43297  climlimsupcex  43317  icccncfext  43435  fperdvper  43467  dvdivbd  43471  dvdsn1add  43487  dvmptfprodlem  43492  dvnprodlem3  43496  fourierdlem10  43665  fourierdlem19  43674  fourierdlem20  43675  fourierdlem35  43690  fourierdlem40  43695  fourierdlem41  43696  fourierdlem42  43697  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem68  43722  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem79  43733  fourierdlem80  43734  elaa2  43782  etransclem35  43817  etransclem38  43820  fge0npnf  43912  sge0tsms  43925  sge0rern  43933  sge0supre  43934  sge0le  43952  sge0fodjrnlem  43961  sge0rpcpnf  43966  meadjun  44007  meadjiunlem  44010  hoidmvlelem2  44141  hspdifhsp  44161  ovolval4lem1  44194