Theorem pm2.65da 828

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  condan  829  nelrdva  3667  eqsnuniex  5332  onnseq  8330  oeeulem  8586  disjen  9121  cantnflem1  9657  ssfin4  10293  fin1a2lem12  10394  fin1a2lem13  10395  canthnumlem  10632  canthwelem  10634  supaddc  12181  supmul1  12183  ixxdisj  13386  ixxub  13392  ixxlb  13393  icodisj  13502  discr1  14275  hashpss  14446  01sqrexlem7  15299  bitsfzolem  16491  bitsfzo  16492  sqnprm  16760  mreexexlem2d  17700  acsinfd  18611  simpgntrivd  20169  prmgrpsimpgd  20185  ablsimpgprmd  20186  ornglmullt  20951  orngrmullt  20952  lbsextlem3  21263  lbsextlem4  21264  pidlnz  21353  drngidl  21364  0ringprmidl  21456  qsidomlem1  21459  iunconn  23564  dissnlocfin  23665  ptcmplem4  24191  iccntr  24958  evth  25097  bcthlem5  25466  ovolicopnf  25662  vitalilem4  25749  dvferm1  26123  dvferm2  26125  dgreq0  26401  radcnvle  26559  isosctrlem2  26960  dmlogdmgm  27164  mersenne  27367  2sqn0  27574  pntlem3  27749  ostth2lem1  27758  tgbtwnne  28735  tglowdim1i  28746  tgbtwndiff  28751  tgbtwnconn1lem3  28819  legso  28844  tglineintmo  28891  tglineneq  28894  tglowdim2ln  28901  tglnpt4  28904  mirne  28920  mirhl  28932  krippenlem  28943  midexlem  28945  footexALT  28973  footexlem2  28975  colperpexlem3  28988  mideulem2  28990  opphllem  28991  oppnid  29002  opphllem2  29004  outpasch  29012  hlpasch  29013  hpgerlem  29022  colhp  29027  trgcopy  29088  tgasa1  29148  prlnghpg  29169  prlngmolem1  29175  prlngmolem2  29176  prlngpln4  29180  umgrnloop2  29462  ex-natded5.5  30727  ex-natded5.8  30730  ex-natded5.13  30732  unidifsnne  32848  ifnefals  32860  rexmul2  33065  nn0min  33131  ccatws1f1o  33237  elrgspnlem2  33529  fracfld  33595  0nellinds  33651  drngidlhash  33707  mxidlirredi  33720  krull  33727  qsdrngi  33743  qsdrng  33745  rsprprmprmidlb  33779  rprmasso2  33782  1arithidom  33793  pidufd  33799  1arithufdlem3  33802  dfufd2  33806  0ringmon1p  33813  ig1pnunit  33857  mplmulmvr  33895  evlextv  33898  esplyfv  33926  esplyfval1  33929  esplyind  33931  vietadeg1  33934  exsslsb  33953  lvecdim0  33963  lindsunlem  33980  assafld  33993  fldextrspundgdvdslem  34036  extdgfialglem1  34048  irredminply  34072  constrextdg2lem  34104  constrext2chnlem  34106  2sqr3nconstr  34137  cos9thpinconstrlem2  34146  zarcls1  34225  zarclsint  34228  qqhre  34376  esumcvgre  34447  carsgclctunlem2  34675  oddpwdc  34710  eulerpartlemf  34726  ballotlemfc0  34849  ballotlemfcc  34850  ballotlemimin  34862  ballotlem1c  34864  reprinfz1  34975  bnj1417  35395  ttcwf2  37002  unbdqndv2lem2  37065  knoppndvlem13  37079  irrdiff  37936  topdifinffinlem  37959  pibt2  38029  poimirlem11  38248  poimirlem12  38249  aks4d1p7  42818  aks4d1p8d2  42820  aks4d1p8  42822  aks4d1p9  42823  fldhmf1  42825  hashscontpow1  42856  aks6d1c5  42874  imo72b2  44868  iunconnlem2  45613  n0p  45735  uzwo4  45743  ssnct  45767  nsstr  45783  disjrnmpt2  45876  difmap  45893  difmapsn  45898  mapssbi  45899  xrlexaddrp  46038  infleinflem2  46056  xrralrecnnge  46075  supminfxr2  46153  xrpnf  46169  icoub  46212  ioonct  46223  ressioosup  46241  ressiooinf  46243  limclner  46335  limsupub  46388  climxrrelem  46433  climlimsupcex  46453  icccncfext  46571  fperdvper  46603  dvdivbd  46607  dvdsn1add  46623  dvmptfprodlem  46628  dvnprodlem3  46632  fourierdlem10  46801  fourierdlem19  46810  fourierdlem20  46811  fourierdlem35  46826  fourierdlem40  46831  fourierdlem41  46832  fourierdlem42  46833  fourierdlem46  46836  fourierdlem48  46838  fourierdlem49  46839  fourierdlem57  46847  fourierdlem58  46848  fourierdlem59  46849  fourierdlem63  46853  fourierdlem64  46854  fourierdlem65  46855  fourierdlem68  46858  fourierdlem74  46864  fourierdlem75  46865  fourierdlem78  46868  fourierdlem79  46869  fourierdlem80  46870  elaa2  46918  etransclem35  46953  etransclem38  46956  fge0npnf  47051  sge0tsms  47064  sge0rern  47072  sge0supre  47073  sge0le  47091  sge0fodjrnlem  47100  sge0rpcpnf  47105  meadjun  47146  meadjiunlem  47149  hoidmvlelem2  47280  hspdifhsp  47300  ovolval4lem1  47333