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  3671  eqsnuniex  5323  onnseq  8319  oeeulem  8575  disjen  9110  cantnflem1  9646  ssfin4  10282  fin1a2lem12  10383  fin1a2lem13  10384  canthnumlem  10621  canthwelem  10623  supaddc  12173  supmul1  12175  ixxdisj  13378  ixxub  13384  ixxlb  13385  icodisj  13494  discr1  14266  01sqrexlem7  15289  bitsfzolem  16482  bitsfzo  16483  sqnprm  16751  mreexexlem2d  17691  acsinfd  18602  simpgntrivd  20161  prmgrpsimpgd  20177  ablsimpgprmd  20178  ornglmullt  20941  orngrmullt  20942  lbsextlem3  21253  lbsextlem4  21254  0ringprmidl  21437  qsidomlem1  21440  iunconn  23546  dissnlocfin  23647  ptcmplem4  24173  iccntr  24940  evth  25079  bcthlem5  25448  ovolicopnf  25644  vitalilem4  25731  dvferm1  26105  dvferm2  26107  dgreq0  26383  radcnvle  26541  isosctrlem2  26942  dmlogdmgm  27146  mersenne  27349  2sqn0  27556  pntlem3  27731  ostth2lem1  27740  tgbtwnne  28717  tglowdim1i  28728  tgbtwndiff  28733  tgbtwnconn1lem3  28801  legso  28826  tglineintmo  28869  tglineneq  28872  tglowdim2ln  28879  tglnpt4  28882  mirne  28898  mirhl  28910  krippenlem  28921  midexlem  28923  footexALT  28949  footexlem2  28951  colperpexlem3  28963  mideulem2  28965  opphllem  28966  oppnid  28977  opphllem2  28979  outpasch  28986  hlpasch  28987  hpgerlem  28996  colhp  29001  trgcopy  29056  tgasa1  29110  umgrnloop2  29405  ex-natded5.5  30670  ex-natded5.8  30673  ex-natded5.13  30675  unidifsnne  32792  ifnefals  32804  rexmul2  33011  hashpss  33066  nn0min  33078  ccatws1f1o  33184  elrgspnlem2  33476  fracfld  33544  0nellinds  33600  pidlnz  33605  drngidl  33657  drngidlhash  33658  mxidlirredi  33671  krull  33678  qsdrngi  33694  qsdrng  33696  rsprprmprmidlb  33730  rprmasso2  33733  1arithidom  33744  pidufd  33750  1arithufdlem3  33753  dfufd2  33757  0ringmon1p  33764  ig1pnunit  33808  mplmulmvr  33846  evlextv  33849  esplyfv  33877  esplyfval1  33880  esplyind  33882  vietadeg1  33885  exsslsb  33904  lvecdim0  33914  lindsunlem  33931  assafld  33944  fldextrspundgdvdslem  33987  extdgfialglem1  33999  irredminply  34023  constrextdg2lem  34055  constrext2chnlem  34057  2sqr3nconstr  34088  cos9thpinconstrlem2  34097  zarcls1  34176  zarclsint  34179  qqhre  34327  esumcvgre  34398  carsgclctunlem2  34626  oddpwdc  34661  eulerpartlemf  34677  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemimin  34813  ballotlem1c  34815  reprinfz1  34926  bnj1417  35346  ttcwf2  36898  unbdqndv2lem2  36961  knoppndvlem13  36975  irrdiff  37830  topdifinffinlem  37853  pibt2  37923  poimirlem11  38142  poimirlem12  38143  aks4d1p7  42712  aks4d1p8d2  42714  aks4d1p8  42716  aks4d1p9  42717  fldhmf1  42719  hashscontpow1  42750  aks6d1c5  42768  imo72b2  44760  iunconnlem2  45508  n0p  45623  uzwo4  45631  ssnct  45655  nsstr  45671  disjrnmpt2  45764  difmap  45781  difmapsn  45786  mapssbi  45787  xrlexaddrp  45926  infleinflem2  45944  xrralrecnnge  45963  supminfxr2  46041  xrpnf  46057  icoub  46100  ioonct  46111  ressioosup  46129  ressiooinf  46131  limclner  46223  limsupub  46276  climxrrelem  46321  climlimsupcex  46341  icccncfext  46459  fperdvper  46491  dvdivbd  46495  dvdsn1add  46511  dvmptfprodlem  46516  dvnprodlem3  46520  fourierdlem10  46689  fourierdlem19  46698  fourierdlem20  46699  fourierdlem35  46714  fourierdlem40  46719  fourierdlem41  46720  fourierdlem42  46721  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem57  46735  fourierdlem58  46736  fourierdlem59  46737  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem68  46746  fourierdlem74  46752  fourierdlem75  46753  fourierdlem78  46756  fourierdlem79  46757  fourierdlem80  46758  elaa2  46806  etransclem35  46841  etransclem38  46844  fge0npnf  46939  sge0tsms  46952  sge0rern  46960  sge0supre  46961  sge0le  46979  sge0fodjrnlem  46988  sge0rpcpnf  46993  meadjun  47034  meadjiunlem  47037  hoidmvlelem2  47168  hspdifhsp  47188  ovolval4lem1  47221