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  3664  eqsnuniex  5307  onnseq  8278  oeeulem  8531  disjen  9066  cantnflem1  9602  ssfin4  10224  fin1a2lem12  10325  fin1a2lem13  10326  canthnumlem  10563  canthwelem  10565  supaddc  12113  supmul1  12115  ixxdisj  13280  ixxub  13286  ixxlb  13287  icodisj  13396  discr1  14166  01sqrexlem7  15175  bitsfzolem  16365  bitsfzo  16366  sqnprm  16633  mreexexlem2d  17572  acsinfd  18483  simpgntrivd  20033  prmgrpsimpgd  20049  ablsimpgprmd  20050  ornglmullt  20806  orngrmullt  20807  lbsextlem3  21119  lbsextlem4  21120  iunconn  23376  dissnlocfin  23477  ptcmplem4  24003  iccntr  24770  evth  24918  bcthlem5  25288  ovolicopnf  25485  vitalilem4  25572  dvferm1  25949  dvferm2  25951  dgreq0  26231  radcnvle  26389  isosctrlem2  26789  dmlogdmgm  26994  mersenne  27198  2sqn0  27405  pntlem3  27580  ostth2lem1  27589  tgbtwnne  28545  tglowdim1i  28556  tgbtwndiff  28561  tgbtwnconn1lem3  28629  legso  28654  tglineintmo  28697  tglineneq  28699  tglowdim2ln  28706  mirne  28722  mirhl  28734  krippenlem  28745  midexlem  28747  footexALT  28773  footexlem2  28775  colperpexlem3  28787  mideulem2  28789  opphllem  28790  oppnid  28801  opphllem2  28803  outpasch  28810  hlpasch  28811  hpgerlem  28820  colhp  28825  trgcopy  28859  tgasa1  28913  umgrnloop2  29202  ex-natded5.5  30468  ex-natded5.8  30471  ex-natded5.13  30473  unidifsnne  32593  ifnefals  32605  rexmul2  32815  hashpss  32870  nn0min  32882  ccatws1f1o  33014  elrgspnlem2  33306  fracfld  33371  0nellinds  33432  pidlnz  33438  drngidl  33495  drngidlhash  33496  0ringprmidl  33511  qsidomlem1  33514  mxidlirredi  33533  krull  33541  qsdrngi  33557  qsdrng  33559  rsprprmprmidlb  33585  rprmasso2  33588  1arithidom  33599  pidufd  33605  1arithufdlem3  33608  dfufd2  33612  0ringmon1p  33619  ig1pnunit  33663  mplmulmvr  33685  evlextv  33688  esplyfv  33709  esplyind  33712  vietadeg1  33715  exsslsb  33734  lvecdim0  33744  lindsunlem  33762  assafld  33775  fldextrspundgdvdslem  33818  extdgfialglem1  33830  irredminply  33854  constrextdg2lem  33886  constrext2chnlem  33888  2sqr3nconstr  33919  cos9thpinconstrlem2  33928  zarcls1  34007  zarclsint  34010  qqhre  34158  esumcvgre  34229  carsgclctunlem2  34457  oddpwdc  34492  eulerpartlemf  34508  ballotlemfc0  34631  ballotlemfcc  34632  ballotlemimin  34644  ballotlem1c  34646  reprinfz1  34760  bnj1417  35178  unbdqndv2lem2  36685  knoppndvlem13  36699  irrdiff  37502  topdifinffinlem  37523  pibt2  37593  poimirlem11  37803  poimirlem12  37804  aks4d1p7  42374  aks4d1p8d2  42376  aks4d1p8  42378  aks4d1p9  42379  fldhmf1  42381  hashscontpow1  42412  aks6d1c5  42430  imo72b2  44449  iunconnlem2  45211  n0p  45326  uzwo4  45334  ssnct  45358  nsstr  45375  disjrnmpt2  45468  difmap  45487  difmapsn  45492  mapssbi  45493  xrlexaddrp  45633  infleinflem2  45651  xrralrecnnge  45670  supminfxr2  45749  xrpnf  45765  icoub  45808  ioonct  45819  ressioosup  45837  ressiooinf  45839  limclner  45931  limsupub  45984  climxrrelem  46029  climlimsupcex  46049  icccncfext  46167  fperdvper  46199  dvdivbd  46203  dvdsn1add  46219  dvmptfprodlem  46224  dvnprodlem3  46228  fourierdlem10  46397  fourierdlem19  46406  fourierdlem20  46407  fourierdlem35  46422  fourierdlem40  46427  fourierdlem41  46428  fourierdlem42  46429  fourierdlem46  46432  fourierdlem48  46434  fourierdlem49  46435  fourierdlem57  46443  fourierdlem58  46444  fourierdlem59  46445  fourierdlem63  46449  fourierdlem64  46450  fourierdlem65  46451  fourierdlem68  46454  fourierdlem74  46460  fourierdlem75  46461  fourierdlem78  46464  fourierdlem79  46465  fourierdlem80  46466  elaa2  46514  etransclem35  46549  etransclem38  46552  fge0npnf  46647  sge0tsms  46660  sge0rern  46668  sge0supre  46669  sge0le  46687  sge0fodjrnlem  46696  sge0rpcpnf  46701  meadjun  46742  meadjiunlem  46745  hoidmvlelem2  46876  hspdifhsp  46896  ovolval4lem1  46929