Theorem pm2.65da 824

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

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

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 209  df-an 399

This theorem is referenced by:  condan  825  nelrdva  3662  eqsnuniex  5312  onnseq  8303  oeeulem  8559  disjen  9095  cantnflem1  9634  ssfin4  10257  fin1a2lem12  10358  fin1a2lem13  10359  canthnumlem  10596  canthwelem  10598  supaddc  12149  supmul1  12151  ixxdisj  13354  ixxub  13360  ixxlb  13361  icodisj  13470  discr1  14242  01sqrexlem7  15251  bitsfzolem  16444  bitsfzo  16445  sqnprm  16713  mreexexlem2d  17653  acsinfd  18564  simpgntrivd  20116  prmgrpsimpgd  20132  ablsimpgprmd  20133  ornglmullt  20891  orngrmullt  20892  lbsextlem3  21203  lbsextlem4  21204  iunconn  23461  dissnlocfin  23562  ptcmplem4  24088  iccntr  24855  evth  24994  bcthlem5  25363  ovolicopnf  25559  vitalilem4  25646  dvferm1  26020  dvferm2  26022  dgreq0  26298  radcnvle  26453  isosctrlem2  26854  dmlogdmgm  27058  mersenne  27261  2sqn0  27468  pntlem3  27643  ostth2lem1  27652  tgbtwnne  28629  tglowdim1i  28640  tgbtwndiff  28645  tgbtwnconn1lem3  28713  legso  28738  tglineintmo  28781  tglineneq  28783  tglowdim2ln  28790  mirne  28806  mirhl  28818  krippenlem  28829  midexlem  28831  footexALT  28857  footexlem2  28859  colperpexlem3  28871  mideulem2  28873  opphllem  28874  oppnid  28885  opphllem2  28887  outpasch  28894  hlpasch  28895  hpgerlem  28904  colhp  28909  trgcopy  28943  tgasa1  28997  umgrnloop2  29286  ex-natded5.5  30551  ex-natded5.8  30554  ex-natded5.13  30556  unidifsnne  32677  ifnefals  32689  rexmul2  32899  hashpss  32954  nn0min  32966  ccatws1f1o  33083  elrgspnlem2  33378  fracfld  33449  0nellinds  33510  pidlnz  33516  drngidl  33573  drngidlhash  33574  0ringprmidl  33590  qsidomlem1  33593  mxidlirredi  33613  krull  33621  qsdrngi  33637  qsdrng  33639  rsprprmprmidlb  33673  rprmasso2  33676  1arithidom  33687  pidufd  33693  1arithufdlem3  33696  dfufd2  33700  0ringmon1p  33707  ig1pnunit  33751  mplmulmvr  33790  evlextv  33793  esplyfv  33821  esplyfval1  33824  esplyind  33826  vietadeg1  33829  exsslsb  33848  lvecdim0  33858  lindsunlem  33875  assafld  33888  fldextrspundgdvdslem  33931  extdgfialglem1  33943  irredminply  33967  constrextdg2lem  33999  constrext2chnlem  34001  2sqr3nconstr  34032  cos9thpinconstrlem2  34041  zarcls1  34120  zarclsint  34123  qqhre  34271  esumcvgre  34342  carsgclctunlem2  34570  oddpwdc  34605  eulerpartlemf  34621  ballotlemfc0  34744  ballotlemfcc  34745  ballotlemimin  34757  ballotlem1c  34759  reprinfz1  34873  bnj1417  35293  ttcwf2  36833  unbdqndv2lem2  36896  knoppndvlem13  36910  irrdiff  37766  topdifinffinlem  37789  pibt2  37859  poimirlem11  38078  poimirlem12  38079  aks4d1p7  42648  aks4d1p8d2  42650  aks4d1p8  42652  aks4d1p9  42653  fldhmf1  42655  hashscontpow1  42686  aks6d1c5  42704  imo72b2  44696  iunconnlem2  45458  n0p  45573  uzwo4  45581  ssnct  45605  nsstr  45621  disjrnmpt2  45714  difmap  45731  difmapsn  45736  mapssbi  45737  xrlexaddrp  45876  infleinflem2  45894  xrralrecnnge  45913  supminfxr2  45991  xrpnf  46007  icoub  46050  ioonct  46061  ressioosup  46079  ressiooinf  46081  limclner  46173  limsupub  46226  climxrrelem  46271  climlimsupcex  46291  icccncfext  46409  fperdvper  46441  dvdivbd  46445  dvdsn1add  46461  dvmptfprodlem  46466  dvnprodlem3  46470  fourierdlem10  46639  fourierdlem19  46648  fourierdlem20  46649  fourierdlem35  46664  fourierdlem40  46669  fourierdlem41  46670  fourierdlem42  46671  fourierdlem46  46674  fourierdlem48  46676  fourierdlem49  46677  fourierdlem57  46685  fourierdlem58  46686  fourierdlem59  46687  fourierdlem63  46691  fourierdlem64  46692  fourierdlem65  46693  fourierdlem68  46696  fourierdlem74  46702  fourierdlem75  46703  fourierdlem78  46706  fourierdlem79  46707  fourierdlem80  46708  elaa2  46756  etransclem35  46791  etransclem38  46794  fge0npnf  46889  sge0tsms  46902  sge0rern  46910  sge0supre  46911  sge0le  46929  sge0fodjrnlem  46938  sge0rpcpnf  46943  meadjun  46984  meadjiunlem  46987  hoidmvlelem2  47118  hspdifhsp  47138  ovolval4lem1  47171