Theorem pm2.65da 822

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

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

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 208  df-an 397

This theorem is referenced by:  condan  823  nelrdva  3653  eqsnuniex  5297  onnseq  8281  oeeulem  8534  disjen  9069  cantnflem1  9608  ssfin4  10230  fin1a2lem12  10331  fin1a2lem13  10332  canthnumlem  10569  canthwelem  10571  supaddc  12121  supmul1  12123  ixxdisj  13311  ixxub  13317  ixxlb  13318  icodisj  13427  discr1  14199  01sqrexlem7  15208  bitsfzolem  16401  bitsfzo  16402  sqnprm  16670  mreexexlem2d  17609  acsinfd  18520  simpgntrivd  20073  prmgrpsimpgd  20089  ablsimpgprmd  20090  ornglmullt  20848  orngrmullt  20849  lbsextlem3  21160  lbsextlem4  21161  iunconn  23418  dissnlocfin  23519  ptcmplem4  24045  iccntr  24812  evth  24951  bcthlem5  25320  ovolicopnf  25516  vitalilem4  25603  dvferm1  25977  dvferm2  25979  dgreq0  26255  radcnvle  26410  isosctrlem2  26808  dmlogdmgm  27012  mersenne  27215  2sqn0  27422  pntlem3  27597  ostth2lem1  27606  tgbtwnne  28583  tglowdim1i  28594  tgbtwndiff  28599  tgbtwnconn1lem3  28667  legso  28692  tglineintmo  28735  tglineneq  28737  tglowdim2ln  28744  mirne  28760  mirhl  28772  krippenlem  28783  midexlem  28785  footexALT  28811  footexlem2  28813  colperpexlem3  28825  mideulem2  28827  opphllem  28828  oppnid  28839  opphllem2  28841  outpasch  28848  hlpasch  28849  hpgerlem  28858  colhp  28863  trgcopy  28897  tgasa1  28951  umgrnloop2  29240  ex-natded5.5  30505  ex-natded5.8  30508  ex-natded5.13  30510  unidifsnne  32631  ifnefals  32643  rexmul2  32853  hashpss  32908  nn0min  32920  ccatws1f1o  33037  elrgspnlem2  33331  fracfld  33399  0nellinds  33460  pidlnz  33466  drngidl  33523  drngidlhash  33524  0ringprmidl  33539  qsidomlem1  33542  mxidlirredi  33561  krull  33569  qsdrngi  33585  qsdrng  33587  rsprprmprmidlb  33613  rprmasso2  33616  1arithidom  33627  pidufd  33633  1arithufdlem3  33636  dfufd2  33640  0ringmon1p  33647  ig1pnunit  33691  mplmulmvr  33730  evlextv  33733  esplyfv  33761  esplyfval1  33764  esplyind  33766  vietadeg1  33769  exsslsb  33788  lvecdim0  33798  lindsunlem  33815  assafld  33828  fldextrspundgdvdslem  33871  extdgfialglem1  33883  irredminply  33907  constrextdg2lem  33939  constrext2chnlem  33941  2sqr3nconstr  33972  cos9thpinconstrlem2  33981  zarcls1  34060  zarclsint  34063  qqhre  34211  esumcvgre  34282  carsgclctunlem2  34510  oddpwdc  34545  eulerpartlemf  34561  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemimin  34697  ballotlem1c  34699  reprinfz1  34813  bnj1417  35230  ttcwf2  36754  unbdqndv2lem2  36817  knoppndvlem13  36831  irrdiff  37687  topdifinffinlem  37710  pibt2  37780  poimirlem11  37999  poimirlem12  38000  aks4d1p7  42569  aks4d1p8d2  42571  aks4d1p8  42573  aks4d1p9  42574  fldhmf1  42576  hashscontpow1  42607  aks6d1c5  42625  imo72b2  44617  iunconnlem2  45379  n0p  45494  uzwo4  45502  ssnct  45526  nsstr  45543  disjrnmpt2  45636  difmap  45653  difmapsn  45658  mapssbi  45659  xrlexaddrp  45798  infleinflem2  45816  xrralrecnnge  45835  supminfxr2  45913  xrpnf  45929  icoub  45972  ioonct  45983  ressioosup  46001  ressiooinf  46003  limclner  46095  limsupub  46148  climxrrelem  46193  climlimsupcex  46213  icccncfext  46331  fperdvper  46363  dvdivbd  46367  dvdsn1add  46383  dvmptfprodlem  46388  dvnprodlem3  46392  fourierdlem10  46561  fourierdlem19  46570  fourierdlem20  46571  fourierdlem35  46586  fourierdlem40  46591  fourierdlem41  46592  fourierdlem42  46593  fourierdlem46  46596  fourierdlem48  46598  fourierdlem49  46599  fourierdlem57  46607  fourierdlem58  46608  fourierdlem59  46609  fourierdlem63  46613  fourierdlem64  46614  fourierdlem65  46615  fourierdlem68  46618  fourierdlem74  46624  fourierdlem75  46625  fourierdlem78  46628  fourierdlem79  46629  fourierdlem80  46630  elaa2  46678  etransclem35  46713  etransclem38  46716  fge0npnf  46811  sge0tsms  46824  sge0rern  46832  sge0supre  46833  sge0le  46851  sge0fodjrnlem  46860  sge0rpcpnf  46865  meadjun  46906  meadjiunlem  46909  hoidmvlelem2  47040  hspdifhsp  47060  ovolval4lem1  47093