Theorem pm2.65da 829

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  condan  830  nelrdva  3666  eqsnuniex  5330  onnseq  8336  oeeulem  8592  disjen  9135  cantnflem1  9671  ssfin4  10315  fin1a2lem12  10416  fin1a2lem13  10417  canthnumlem  10660  canthwelem  10662  supaddc  12209  supmul1  12211  ixxdisj  13415  ixxub  13421  ixxlb  13422  icodisj  13531  discr1  14305  hashpss  14476  01sqrexlem7  15337  bitsfzolem  16528  bitsfzo  16529  sqnprm  16797  mreexexlem2d  17737  acsinfd  18648  simpgntrivd  20231  prmgrpsimpgd  20247  ablsimpgprmd  20248  ornglmullt  21039  orngrmullt  21040  lbsextlem3  21351  lbsextlem4  21352  pidlnz  21441  drngidl  21452  0ringprmidl  21544  qsidomlem1  21547  iunconn  23657  dissnlocfin  23759  ptcmplem4  24285  iccntr  25052  evth  25191  bcthlem5  25560  ovolicopnf  25756  vitalilem4  25843  dvferm1  26217  dvferm2  26219  dgreq0  26495  radcnvle  26656  isosctrlem2  27057  dmlogdmgm  27261  mersenne  27464  2sqn0  27671  pntlem3  27846  ostth2lem1  27855  tgbtwnne  28833  tglowdim1i  28844  tgbtwndiff  28849  tgbtwnconn1lem3  28917  legso  28942  tglineintmo  28990  tglineneq  28993  tglowdim2ln  29000  tglnpt4  29003  mirne  29019  mirhl  29031  krippenlem  29042  midexlem  29044  symquadprlnglem  29045  footexALT  29073  footexlem2  29075  colperpexlem3  29088  mideulem2  29090  opphllem  29091  oppnid  29102  opphllem2  29104  outpasch  29113  hlpasch  29114  hpgerlem  29123  colhp  29128  trgcopy  29191  tgaaddcpbllem1  29229  tgaaddcpbl  29232  tgasa1  29283  prlnghpg  29304  prlngmolem1  29310  prlngmolem2  29311  prlngpln4  29316  prlngsymquadlem  29321  umgrnloop2  29604  ex-natded5.5  30891  ex-natded5.8  30894  ex-natded5.13  30896  unidifsnne  33012  ifnefals  33024  rexmul2  33227  nn0min  33293  ccatws1f1o  33395  elrgspnlem2  33685  fracfld  33751  0nellinds  33807  drngidlhash  33863  mxidlirredi  33876  krull  33883  qsdrngi  33899  qsdrng  33901  rsprprmprmidlb  33935  rprmasso2  33938  1arithidom  33949  pidufd  33955  1arithufdlem3  33958  dfufd2  33962  0ringmon1p  33969  ig1pnunit  34013  mplmulmvr  34051  evlextv  34054  esplyfv  34082  esplyfval1  34085  esplyind  34087  vietadeg1  34090  exsslsb  34109  lvecdim0  34119  lindsunlem  34136  assafld  34149  fldextrspundgdvdslem  34192  extdgfialglem1  34204  irredminply  34228  constrextdg2lem  34260  constrext2chnlem  34262  2sqr3nconstr  34293  cos9thpinconstrlem2  34302  zarcls1  34381  zarclsint  34384  qqhre  34532  esumcvgre  34603  carsgclctunlem2  34832  oddpwdc  34867  eulerpartlemf  34883  ballotlemfc0  35006  ballotlemfcc  35007  ballotlemimin  35019  ballotlem1c  35021  reprinfz1  35132  bnj1417  35552  ttcwf2  37146  unbdqndv2lem2  37209  knoppndvlem13  37223  irrdiff  38080  topdifinffinlem  38103  pibt2  38173  poimirlem11  38382  poimirlem12  38383  aks4d1p7  42951  aks4d1p8d2  42953  aks4d1p8  42955  aks4d1p9  42956  fldhmf1  42958  hashscontpow1  42989  aks6d1c5  43007  imo72b2  45014  iunconnlem2  45759  n0p  45881  uzwo4  45889  ssnct  45913  nsstr  45929  disjrnmpt2  46022  difmap  46039  difmapsn  46044  mapssbi  46045  xrlexaddrp  46184  infleinflem2  46202  xrralrecnnge  46221  supminfxr2  46299  xrpnf  46315  icoub  46358  ioonct  46369  ressioosup  46387  ressiooinf  46389  limclner  46481  limsupub  46534  climxrrelem  46579  climlimsupcex  46599  icccncfext  46717  fperdvper  46749  dvdivbd  46753  dvdsn1add  46769  dvmptfprodlem  46774  dvnprodlem3  46778  fourierdlem10  46947  fourierdlem19  46956  fourierdlem20  46957  fourierdlem35  46972  fourierdlem40  46977  fourierdlem41  46978  fourierdlem42  46979  fourierdlem46  46982  fourierdlem48  46984  fourierdlem49  46985  fourierdlem57  46993  fourierdlem58  46994  fourierdlem59  46995  fourierdlem63  46999  fourierdlem64  47000  fourierdlem65  47001  fourierdlem68  47004  fourierdlem74  47010  fourierdlem75  47011  fourierdlem78  47014  fourierdlem79  47015  fourierdlem80  47016  elaa2  47064  etransclem35  47099  etransclem38  47102  fge0npnf  47197  sge0tsms  47210  sge0rern  47218  sge0supre  47219  sge0le  47237  sge0fodjrnlem  47246  sge0rpcpnf  47251  meadjun  47292  meadjiunlem  47295  hoidmvlelem2  47426  hspdifhsp  47446  ovolval4lem1  47479