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  8353  oeeulem  8611  disjen  9154  cantnflem1  9691  ssfin4  10389  fin1a2lem12  10490  fin1a2lem13  10491  canthnumlem  10734  canthwelem  10736  supaddc  12285  supmul1  12287  ixxdisj  13492  ixxub  13498  ixxlb  13499  icodisj  13608  discr1  14384  hashpss  14555  01sqrexlem7  15416  bitsfzolem  16605  bitsfzo  16606  sqnprm  16879  mreexexlem2d  17820  acsinfd  18731  simpgntrivd  20315  prmgrpsimpgd  20331  ablsimpgprmd  20332  ornglmullt  21127  orngrmullt  21128  lbsextlem3  21439  lbsextlem4  21440  pidlnz  21529  drngidl  21540  0ringprmidl  21634  qsidomlem1  21637  iunconn  23747  dissnlocfin  23849  ptcmplem4  24375  iccntr  25142  evth  25281  bcthlem5  25650  ovolicopnf  25846  vitalilem4  25933  dvferm1  26306  dvferm2  26308  dgreq0  26585  radcnvle  26748  isosctrlem2  27148  dmlogdmgm  27352  mersenne  27555  2sqn0  27762  pntlem3  27937  ostth2lem1  27946  tgbtwnne  28954  tglowdim1i  28965  tgbtwndiff  28970  tgbtwnconn1lem3  29038  legso  29063  tglineintmo  29111  tglineneq  29114  tglowdim2ln  29121  tglnpt4  29124  mirne  29140  mirhl  29152  krippenlem  29163  midexlem  29165  symquadprlnglem  29166  footexALT  29194  footexlem2  29196  colperpexlem3  29209  mideulem2  29211  opphllem  29212  oppnid  29223  opphllem2  29225  outpasch  29234  hlpasch  29235  hpgerlem  29244  colhp  29249  trgcopy  29312  tgaaddcpbllem1  29350  tgaaddcpbl  29353  tgasa1  29404  prlnghpg  29425  prlngmolem1  29431  prlngmolem2  29432  prlngpln4  29437  prlngsymquadlem  29442  umgrnloop2  29725  ex-natded5.5  31012  ex-natded5.8  31015  ex-natded5.13  31017  unidifsnne  33175  ifnefals  33187  rexmul2  33389  nn0min  33455  ccatws1f1o  33557  elrgspnlem2  33847  fracfld  33913  0nellinds  33969  drngidlhash  34026  mxidlirredi  34039  krull  34046  qsdrngi  34062  qsdrng  34064  rsprprmprmidlb  34098  rprmasso2  34101  1arithidom  34112  pidufd  34118  1arithufdlem3  34121  dfufd2  34125  0ringmon1p  34132  ig1pnunit  34176  mplmulmvr  34214  evlextv  34217  esplyfv  34245  esplyfval1  34248  esplyind  34250  vietadeg1  34253  exsslsb  34272  lvecdim0  34282  lindsunlem  34299  assafld  34312  fldextrspundgdvdslem  34355  extdgfialglem1  34367  irredminply  34391  constrextdg2lem  34423  constrext2chnlem  34425  2sqr3nconstr  34456  cos9thpinconstrlem2  34465  zarcls1  34544  zarclsint  34547  qqhre  34695  esumcvgre  34766  carsgclctunlem2  34994  oddpwdc  35029  eulerpartlemf  35045  ballotlemfc0  35168  ballotlemfcc  35169  ballotlemimin  35181  ballotlem1c  35183  reprinfz1  35294  bnj1417  35714  ttcwf2  37388  unbdqndv2lem2  37451  knoppndvlem13  37465  irrdiff  38323  topdifinffinlem  38346  pibt2  38416  poimirlem11  38625  poimirlem12  38626  aks4d1p7  43209  aks4d1p8d2  43211  aks4d1p8  43213  aks4d1p9  43214  fldhmf1  43216  hashscontpow1  43247  aks6d1c5  43265  imo72b2  45248  iunconnlem2  45993  n0p  46138  uzwo4  46146  ssnct  46170  nsstr  46186  disjrnmpt2  46279  difmap  46296  difmapsn  46301  mapssbi  46302  xrlexaddrp  46440  infleinflem2  46458  xrralrecnnge  46477  supminfxr2  46555  xrpnf  46571  icoub  46614  ioonct  46625  ressioosup  46643  ressiooinf  46645  limclner  46737  limsupub  46790  climxrrelem  46835  climlimsupcex  46855  icccncfext  46973  fperdvper  47005  dvdivbd  47009  dvdsn1add  47025  dvmptfprodlem  47030  dvnprodlem3  47034  fourierdlem10  47203  fourierdlem19  47212  fourierdlem20  47213  fourierdlem35  47228  fourierdlem40  47233  fourierdlem41  47234  fourierdlem42  47235  fourierdlem46  47238  fourierdlem48  47240  fourierdlem49  47241  fourierdlem57  47249  fourierdlem58  47250  fourierdlem59  47251  fourierdlem63  47255  fourierdlem64  47256  fourierdlem65  47257  fourierdlem68  47260  fourierdlem74  47266  fourierdlem75  47267  fourierdlem78  47270  fourierdlem79  47271  fourierdlem80  47272  elaa2  47320  etransclem35  47355  etransclem38  47358  fge0npnf  47453  sge0tsms  47466  sge0rern  47474  sge0supre  47475  sge0le  47493  sge0fodjrnlem  47502  sge0rpcpnf  47507  meadjun  47548  meadjiunlem  47551  hoidmvlelem2  47682  hspdifhsp  47702  ovolval4lem1  47735