Theorem pm2.65da 816

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  817  nelrdva  3727  eqsnuniex  5379  onnseq  8400  oeeulem  8657  disjen  9200  cantnflem1  9758  ssfin4  10379  fin1a2lem12  10480  fin1a2lem13  10481  canthnumlem  10717  canthwelem  10719  supaddc  12262  supmul1  12264  ixxdisj  13422  ixxub  13428  ixxlb  13429  icodisj  13536  discr1  14288  01sqrexlem7  15297  bitsfzolem  16480  bitsfzo  16481  sqnprm  16749  mreexexlem2d  17703  acsinfd  18626  simpgntrivd  20142  prmgrpsimpgd  20158  ablsimpgprmd  20159  lbsextlem3  21185  lbsextlem4  21186  iunconn  23457  dissnlocfin  23558  ptcmplem4  24084  iccntr  24862  evth  25010  bcthlem5  25381  ovolicopnf  25578  vitalilem4  25665  dvferm1  26043  dvferm2  26045  dgreq0  26325  radcnvle  26481  isosctrlem2  26880  dmlogdmgm  27085  mersenne  27289  2sqn0  27496  pntlem3  27671  ostth2lem1  27680  tgbtwnne  28516  tglowdim1i  28527  tgbtwndiff  28532  tgbtwnconn1lem3  28600  legso  28625  tglineintmo  28668  tglineneq  28670  tglowdim2ln  28677  mirne  28693  mirhl  28705  krippenlem  28716  midexlem  28718  footexALT  28744  footexlem2  28746  colperpexlem3  28758  mideulem2  28760  opphllem  28761  oppnid  28772  opphllem2  28774  outpasch  28781  hlpasch  28782  hpgerlem  28791  colhp  28796  trgcopy  28830  tgasa1  28884  umgrnloop2  29181  ex-natded5.5  30442  ex-natded5.8  30445  ex-natded5.13  30447  unidifsnne  32564  ifnefals  32571  nn0min  32824  ccatws1f1o  32918  fracfld  33275  ornglmullt  33302  orngrmullt  33303  0nellinds  33363  pidlnz  33369  drngidl  33426  drngidlhash  33427  0ringprmidl  33442  qsidomlem1  33445  mxidlirredi  33464  krull  33472  qsdrngi  33488  qsdrng  33490  rsprprmprmidlb  33516  rprmasso2  33519  1arithidom  33530  pidufd  33536  1arithufdlem3  33539  dfufd2  33543  0ringmon1p  33548  ig1pnunit  33586  lvecdim0  33619  lindsunlem  33637  assafld  33650  irredminply  33707  zarcls1  33815  zarclsint  33818  qqhre  33966  esumcvgre  34055  carsgclctunlem2  34284  oddpwdc  34319  eulerpartlemf  34335  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemimin  34470  ballotlem1c  34472  reprinfz1  34599  bnj1417  35017  unbdqndv2lem2  36476  knoppndvlem13  36490  irrdiff  37292  topdifinffinlem  37313  pibt2  37383  poimirlem11  37591  poimirlem12  37592  aks4d1p7  42040  aks4d1p8d2  42042  aks4d1p8  42044  aks4d1p9  42045  fldhmf1  42047  hashscontpow1  42078  aks6d1c5  42096  imo72b2  44134  iunconnlem2  44906  n0p  44945  uzwo4  44955  ssnct  44979  nsstr  44997  disjrnmpt2  45095  difmap  45114  difmapsn  45119  mapssbi  45120  xrlexaddrp  45267  infleinflem2  45286  xrralrecnnge  45305  supminfxr2  45384  xrpnf  45401  icoub  45444  ioonct  45455  ressioosup  45473  ressiooinf  45475  limclner  45572  limsupub  45625  climxrrelem  45670  climlimsupcex  45690  icccncfext  45808  fperdvper  45840  dvdivbd  45844  dvdsn1add  45860  dvmptfprodlem  45865  dvnprodlem3  45869  fourierdlem10  46038  fourierdlem19  46047  fourierdlem20  46048  fourierdlem35  46063  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem68  46095  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem79  46106  fourierdlem80  46107  elaa2  46155  etransclem35  46190  etransclem38  46193  fge0npnf  46288  sge0tsms  46301  sge0rern  46309  sge0supre  46310  sge0le  46328  sge0fodjrnlem  46337  sge0rpcpnf  46342  meadjun  46383  meadjiunlem  46386  hoidmvlelem2  46517  hspdifhsp  46537  ovolval4lem1  46570