Theorem pm2.65da 829

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  condan  830  nelrdva  3662  eqsnuniex  5322  onnseq  8330  oeeulem  8588  disjen  9131  cantnflem1  9668  ssfin4  10360  fin1a2lem12  10461  fin1a2lem13  10462  canthnumlem  10705  canthwelem  10707  supaddc  12254  supmul1  12256  ixxdisj  13461  ixxub  13467  ixxlb  13468  icodisj  13577  discr1  14351  hashpss  14522  01sqrexlem7  15383  bitsfzolem  16572  bitsfzo  16573  sqnprm  16841  mreexexlem2d  17781  acsinfd  18692  simpgntrivd  20276  prmgrpsimpgd  20292  ablsimpgprmd  20293  ornglmullt  21088  orngrmullt  21089  lbsextlem3  21400  lbsextlem4  21401  pidlnz  21490  drngidl  21501  0ringprmidl  21595  qsidomlem1  21598  iunconn  23708  dissnlocfin  23810  ptcmplem4  24336  iccntr  25103  evth  25242  bcthlem5  25611  ovolicopnf  25807  vitalilem4  25894  dvferm1  26267  dvferm2  26269  dgreq0  26546  radcnvle  26711  isosctrlem2  27111  dmlogdmgm  27315  mersenne  27518  2sqn0  27725  pntlem3  27900  ostth2lem1  27909  tgbtwnne  28887  tglowdim1i  28898  tgbtwndiff  28903  tgbtwnconn1lem3  28971  legso  28996  tglineintmo  29044  tglineneq  29047  tglowdim2ln  29054  tglnpt4  29057  mirne  29073  mirhl  29085  krippenlem  29096  midexlem  29098  symquadprlnglem  29099  footexALT  29127  footexlem2  29129  colperpexlem3  29142  mideulem2  29144  opphllem  29145  oppnid  29156  opphllem2  29158  outpasch  29167  hlpasch  29168  hpgerlem  29177  colhp  29182  trgcopy  29245  tgaaddcpbllem1  29283  tgaaddcpbl  29286  tgasa1  29337  prlnghpg  29358  prlngmolem1  29364  prlngmolem2  29365  prlngpln4  29370  prlngsymquadlem  29375  umgrnloop2  29658  ex-natded5.5  30945  ex-natded5.8  30948  ex-natded5.13  30950  unidifsnne  33066  ifnefals  33078  rexmul2  33280  nn0min  33346  ccatws1f1o  33448  elrgspnlem2  33738  fracfld  33804  0nellinds  33860  drngidlhash  33917  mxidlirredi  33930  krull  33937  qsdrngi  33953  qsdrng  33955  rsprprmprmidlb  33989  rprmasso2  33992  1arithidom  34003  pidufd  34009  1arithufdlem3  34012  dfufd2  34016  0ringmon1p  34023  ig1pnunit  34067  mplmulmvr  34105  evlextv  34108  esplyfv  34136  esplyfval1  34139  esplyind  34141  vietadeg1  34144  exsslsb  34163  lvecdim0  34173  lindsunlem  34190  assafld  34203  fldextrspundgdvdslem  34246  extdgfialglem1  34258  irredminply  34282  constrextdg2lem  34314  constrext2chnlem  34316  2sqr3nconstr  34347  cos9thpinconstrlem2  34356  zarcls1  34435  zarclsint  34438  qqhre  34586  esumcvgre  34657  carsgclctunlem2  34886  oddpwdc  34921  eulerpartlemf  34937  ballotlemfc0  35060  ballotlemfcc  35061  ballotlemimin  35073  ballotlem1c  35075  reprinfz1  35186  bnj1417  35606  ttcwf2  37235  unbdqndv2lem2  37298  knoppndvlem13  37312  irrdiff  38167  topdifinffinlem  38190  pibt2  38260  poimirlem11  38469  poimirlem12  38470  aks4d1p7  43053  aks4d1p8d2  43055  aks4d1p8  43057  aks4d1p9  43058  fldhmf1  43060  hashscontpow1  43091  aks6d1c5  43109  imo72b2  45116  iunconnlem2  45861  n0p  45983  uzwo4  45991  ssnct  46015  nsstr  46031  disjrnmpt2  46124  difmap  46141  difmapsn  46146  mapssbi  46147  xrlexaddrp  46286  infleinflem2  46304  xrralrecnnge  46323  supminfxr2  46401  xrpnf  46417  icoub  46460  ioonct  46471  ressioosup  46489  ressiooinf  46491  limclner  46583  limsupub  46636  climxrrelem  46681  climlimsupcex  46701  icccncfext  46819  fperdvper  46851  dvdivbd  46855  dvdsn1add  46871  dvmptfprodlem  46876  dvnprodlem3  46880  fourierdlem10  47049  fourierdlem19  47058  fourierdlem20  47059  fourierdlem35  47074  fourierdlem40  47079  fourierdlem41  47080  fourierdlem42  47081  fourierdlem46  47084  fourierdlem48  47086  fourierdlem49  47087  fourierdlem57  47095  fourierdlem58  47096  fourierdlem59  47097  fourierdlem63  47101  fourierdlem64  47102  fourierdlem65  47103  fourierdlem68  47106  fourierdlem74  47112  fourierdlem75  47113  fourierdlem78  47116  fourierdlem79  47117  fourierdlem80  47118  elaa2  47166  etransclem35  47201  etransclem38  47204  fge0npnf  47299  sge0tsms  47312  sge0rern  47320  sge0supre  47321  sge0le  47339  sge0fodjrnlem  47348  sge0rpcpnf  47353  meadjun  47394  meadjiunlem  47397  hoidmvlelem2  47528  hspdifhsp  47548  ovolval4lem1  47581