Theorem pm2.65da 817

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  818  nelrdva  3713  eqsnuniex  5366  onnseq  8382  oeeulem  8637  disjen  9172  cantnflem1  9726  ssfin4  10347  fin1a2lem12  10448  fin1a2lem13  10449  canthnumlem  10685  canthwelem  10687  supaddc  12232  supmul1  12234  ixxdisj  13398  ixxub  13404  ixxlb  13405  icodisj  13512  discr1  14274  01sqrexlem7  15283  bitsfzolem  16467  bitsfzo  16468  sqnprm  16735  mreexexlem2d  17689  acsinfd  18613  simpgntrivd  20132  prmgrpsimpgd  20148  ablsimpgprmd  20149  lbsextlem3  21179  lbsextlem4  21180  iunconn  23451  dissnlocfin  23552  ptcmplem4  24078  iccntr  24856  evth  25004  bcthlem5  25375  ovolicopnf  25572  vitalilem4  25659  dvferm1  26037  dvferm2  26039  dgreq0  26319  radcnvle  26477  isosctrlem2  26876  dmlogdmgm  27081  mersenne  27285  2sqn0  27492  pntlem3  27667  ostth2lem1  27676  tgbtwnne  28512  tglowdim1i  28523  tgbtwndiff  28528  tgbtwnconn1lem3  28596  legso  28621  tglineintmo  28664  tglineneq  28666  tglowdim2ln  28673  mirne  28689  mirhl  28701  krippenlem  28712  midexlem  28714  footexALT  28740  footexlem2  28742  colperpexlem3  28754  mideulem2  28756  opphllem  28757  oppnid  28768  opphllem2  28770  outpasch  28777  hlpasch  28778  hpgerlem  28787  colhp  28792  trgcopy  28826  tgasa1  28880  umgrnloop2  29177  ex-natded5.5  30438  ex-natded5.8  30441  ex-natded5.13  30443  unidifsnne  32561  ifnefals  32568  nn0min  32826  ccatws1f1o  32920  elrgspnlem2  33232  fracfld  33289  ornglmullt  33316  orngrmullt  33317  0nellinds  33377  pidlnz  33383  drngidl  33440  drngidlhash  33441  0ringprmidl  33456  qsidomlem1  33459  mxidlirredi  33478  krull  33486  qsdrngi  33502  qsdrng  33504  rsprprmprmidlb  33530  rprmasso2  33533  1arithidom  33544  pidufd  33550  1arithufdlem3  33553  dfufd2  33557  0ringmon1p  33562  ig1pnunit  33600  lvecdim0  33633  lindsunlem  33651  assafld  33664  irredminply  33721  zarcls1  33829  zarclsint  33832  qqhre  33982  esumcvgre  34071  carsgclctunlem2  34300  oddpwdc  34335  eulerpartlemf  34351  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemimin  34486  ballotlem1c  34488  reprinfz1  34615  bnj1417  35033  unbdqndv2lem2  36492  knoppndvlem13  36506  irrdiff  37308  topdifinffinlem  37329  pibt2  37399  poimirlem11  37617  poimirlem12  37618  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  fldhmf1  42071  hashscontpow1  42102  aks6d1c5  42120  imo72b2  44161  iunconnlem2  44932  n0p  44982  uzwo4  44992  ssnct  45016  nsstr  45034  disjrnmpt2  45130  difmap  45149  difmapsn  45154  mapssbi  45155  xrlexaddrp  45301  infleinflem2  45320  xrralrecnnge  45339  supminfxr2  45418  xrpnf  45435  icoub  45478  ioonct  45489  ressioosup  45507  ressiooinf  45509  limclner  45606  limsupub  45659  climxrrelem  45704  climlimsupcex  45724  icccncfext  45842  fperdvper  45874  dvdivbd  45878  dvdsn1add  45894  dvmptfprodlem  45899  dvnprodlem3  45903  fourierdlem10  46072  fourierdlem19  46081  fourierdlem20  46082  fourierdlem35  46097  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem68  46129  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem80  46141  elaa2  46189  etransclem35  46224  etransclem38  46227  fge0npnf  46322  sge0tsms  46335  sge0rern  46343  sge0supre  46344  sge0le  46362  sge0fodjrnlem  46371  sge0rpcpnf  46376  meadjun  46417  meadjiunlem  46420  hoidmvlelem2  46551  hspdifhsp  46571  ovolval4lem1  46604