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  3665  eqsnuniex  5308  onnseq  8286  oeeulem  8539  disjen  9074  cantnflem1  9610  ssfin4  10232  fin1a2lem12  10333  fin1a2lem13  10334  canthnumlem  10571  canthwelem  10573  supaddc  12121  supmul1  12123  ixxdisj  13288  ixxub  13294  ixxlb  13295  icodisj  13404  discr1  14174  01sqrexlem7  15183  bitsfzolem  16373  bitsfzo  16374  sqnprm  16641  mreexexlem2d  17580  acsinfd  18491  simpgntrivd  20041  prmgrpsimpgd  20057  ablsimpgprmd  20058  ornglmullt  20814  orngrmullt  20815  lbsextlem3  21127  lbsextlem4  21128  iunconn  23384  dissnlocfin  23485  ptcmplem4  24011  iccntr  24778  evth  24926  bcthlem5  25296  ovolicopnf  25493  vitalilem4  25580  dvferm1  25957  dvferm2  25959  dgreq0  26239  radcnvle  26397  isosctrlem2  26797  dmlogdmgm  27002  mersenne  27206  2sqn0  27413  pntlem3  27588  ostth2lem1  27597  tgbtwnne  28574  tglowdim1i  28585  tgbtwndiff  28590  tgbtwnconn1lem3  28658  legso  28683  tglineintmo  28726  tglineneq  28728  tglowdim2ln  28735  mirne  28751  mirhl  28763  krippenlem  28774  midexlem  28776  footexALT  28802  footexlem2  28804  colperpexlem3  28816  mideulem2  28818  opphllem  28819  oppnid  28830  opphllem2  28832  outpasch  28839  hlpasch  28840  hpgerlem  28849  colhp  28854  trgcopy  28888  tgasa1  28942  umgrnloop2  29231  ex-natded5.5  30497  ex-natded5.8  30500  ex-natded5.13  30502  unidifsnne  32622  ifnefals  32634  rexmul2  32844  hashpss  32899  nn0min  32911  ccatws1f1o  33043  elrgspnlem2  33336  fracfld  33401  0nellinds  33462  pidlnz  33468  drngidl  33525  drngidlhash  33526  0ringprmidl  33541  qsidomlem1  33544  mxidlirredi  33563  krull  33571  qsdrngi  33587  qsdrng  33589  rsprprmprmidlb  33615  rprmasso2  33618  1arithidom  33629  pidufd  33635  1arithufdlem3  33638  dfufd2  33642  0ringmon1p  33649  ig1pnunit  33693  mplmulmvr  33715  evlextv  33718  esplyfv  33746  esplyfval1  33749  esplyind  33751  vietadeg1  33754  exsslsb  33773  lvecdim0  33783  lindsunlem  33801  assafld  33814  fldextrspundgdvdslem  33857  extdgfialglem1  33869  irredminply  33893  constrextdg2lem  33925  constrext2chnlem  33927  2sqr3nconstr  33958  cos9thpinconstrlem2  33967  zarcls1  34046  zarclsint  34049  qqhre  34197  esumcvgre  34268  carsgclctunlem2  34496  oddpwdc  34531  eulerpartlemf  34547  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemimin  34683  ballotlem1c  34685  reprinfz1  34799  bnj1417  35216  unbdqndv2lem2  36729  knoppndvlem13  36743  irrdiff  37570  topdifinffinlem  37591  pibt2  37661  poimirlem11  37871  poimirlem12  37872  aks4d1p7  42442  aks4d1p8d2  42444  aks4d1p8  42446  aks4d1p9  42447  fldhmf1  42449  hashscontpow1  42480  aks6d1c5  42498  imo72b2  44517  iunconnlem2  45279  n0p  45394  uzwo4  45402  ssnct  45426  nsstr  45443  disjrnmpt2  45536  difmap  45554  difmapsn  45559  mapssbi  45560  xrlexaddrp  45700  infleinflem2  45718  xrralrecnnge  45737  supminfxr2  45816  xrpnf  45832  icoub  45875  ioonct  45886  ressioosup  45904  ressiooinf  45906  limclner  45998  limsupub  46051  climxrrelem  46096  climlimsupcex  46116  icccncfext  46234  fperdvper  46266  dvdivbd  46270  dvdsn1add  46286  dvmptfprodlem  46291  dvnprodlem3  46295  fourierdlem10  46464  fourierdlem19  46473  fourierdlem20  46474  fourierdlem35  46489  fourierdlem40  46494  fourierdlem41  46495  fourierdlem42  46496  fourierdlem46  46499  fourierdlem48  46501  fourierdlem49  46502  fourierdlem57  46510  fourierdlem58  46511  fourierdlem59  46512  fourierdlem63  46516  fourierdlem64  46517  fourierdlem65  46518  fourierdlem68  46521  fourierdlem74  46527  fourierdlem75  46528  fourierdlem78  46531  fourierdlem79  46532  fourierdlem80  46533  elaa2  46581  etransclem35  46616  etransclem38  46619  fge0npnf  46714  sge0tsms  46727  sge0rern  46735  sge0supre  46736  sge0le  46754  sge0fodjrnlem  46763  sge0rpcpnf  46768  meadjun  46809  meadjiunlem  46812  hoidmvlelem2  46943  hspdifhsp  46963  ovolval4lem1  46996