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  3666  eqsnuniex  5327  onnseq  8380  oeeulem  8638  disjen  9181  cantnflem1  9717  ssfin4  10415  fin1a2lem12  10516  fin1a2lem13  10517  canthnumlem  10760  canthwelem  10762  supaddc  12311  supmul1  12313  ixxdisj  13518  ixxub  13524  ixxlb  13525  icodisj  13634  discr1  14410  hashpss  14581  01sqrexlem7  15444  bitsfzolem  16633  bitsfzo  16634  sqnprm  16907  mreexexlem2d  17848  acsinfd  18759  simpgntrivd  20344  prmgrpsimpgd  20360  ablsimpgprmd  20361  ornglmullt  21156  orngrmullt  21157  lbsextlem3  21468  lbsextlem4  21469  pidlnz  21558  drngidl  21569  0ringprmidl  21663  qsidomlem1  21666  iunconn  23776  dissnlocfin  23878  ptcmplem4  24404  iccntr  25171  evth  25310  bcthlem5  25679  ovolicopnf  25875  vitalilem4  25962  dvferm1  26335  dvferm2  26337  dgreq0  26614  radcnvle  26777  isosctrlem2  27177  dmlogdmgm  27381  mersenne  27584  2sqn0  27791  pntlem3  27966  ostth2lem1  27975  tgbtwnne  28983  tglowdim1i  28994  tgbtwndiff  28999  tgbtwnconn1lem3  29067  legso  29092  tglineintmo  29140  tglineneq  29143  tglowdim2ln  29150  tglnpt4  29153  mirne  29169  mirhl  29181  krippenlem  29192  midexlem  29194  symquadprlnglem  29195  footexALT  29223  footexlem2  29225  colperpexlem3  29238  mideulem2  29240  opphllem  29241  oppnid  29252  opphllem2  29254  outpasch  29263  hlpasch  29264  hpgerlem  29273  colhp  29278  trgcopy  29341  tgaaddcpbllem1  29379  tgaaddcpbl  29382  tgasa1  29433  prlnghpg  29454  prlngmolem1  29460  prlngmolem2  29461  prlngpln4  29466  prlngsymquadlem  29471  umgrnloop2  29754  ex-natded5.5  31041  ex-natded5.8  31044  ex-natded5.13  31046  unidifsnne  33204  ifnefals  33216  rexmul2  33416  nn0min  33482  ccatws1f1o  33584  elrgspnlem2  33874  fracfld  33940  0nellinds  33996  drngidlhash  34053  mxidlirredi  34066  krull  34073  qsdrngi  34089  qsdrng  34091  rsprprmprmidlb  34125  rprmasso2  34128  1arithidom  34139  pidufd  34145  1arithufdlem3  34148  dfufd2  34152  0ringmon1p  34159  ig1pnunit  34203  mplmulmvr  34241  evlextv  34244  esplyfv  34272  esplyfval1  34275  esplyind  34277  vietadeg1  34280  exsslsb  34299  lvecdim0  34309  lindsunlem  34326  assafld  34339  fldextrspundgdvdslem  34382  extdgfialglem1  34394  irredminply  34418  constrextdg2lem  34450  constrext2chnlem  34452  2sqr3nconstr  34483  cos9thpinconstrlem2  34492  zarcls1  34571  zarclsint  34574  qqhre  34722  esumcvgre  34793  carsgclctunlem2  35021  oddpwdc  35056  eulerpartlemf  35072  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemimin  35208  ballotlem1c  35210  reprinfz1  35321  bnj1417  35741  ttcwf2  37491  unbdqndv2lem2  37554  knoppndvlem13  37568  irrdiff  38439  topdifinffinlem  38462  pibt2  38532  poimirlem11  38741  poimirlem12  38742  aks4d1p7  43325  aks4d1p8d2  43327  aks4d1p8  43329  aks4d1p9  43330  fldhmf1  43332  hashscontpow1  43363  aks6d1c5  43381  imo72b2  45364  iunconnlem2  46108  n0p  46267  uzwo4  46275  ssnct  46299  nsstr  46315  disjrnmpt2  46408  difmap  46425  difmapsn  46430  mapssbi  46431  xrlexaddrp  46569  infleinflem2  46587  xrralrecnnge  46606  supminfxr2  46684  xrpnf  46700  icoub  46743  ioonct  46754  ressioosup  46772  ressiooinf  46774  limclner  46866  limsupub  46919  climxrrelem  46964  climlimsupcex  46984  icccncfext  47102  fperdvper  47134  dvdivbd  47138  dvdsn1add  47154  dvmptfprodlem  47159  dvnprodlem3  47163  fourierdlem10  47332  fourierdlem19  47341  fourierdlem20  47342  fourierdlem35  47357  fourierdlem40  47362  fourierdlem41  47363  fourierdlem42  47364  fourierdlem46  47367  fourierdlem48  47369  fourierdlem49  47370  fourierdlem57  47378  fourierdlem58  47379  fourierdlem59  47380  fourierdlem63  47384  fourierdlem64  47385  fourierdlem65  47386  fourierdlem68  47389  fourierdlem74  47395  fourierdlem75  47396  fourierdlem78  47399  fourierdlem79  47400  fourierdlem80  47401  elaa2  47449  etransclem35  47484  etransclem38  47487  fge0npnf  47582  sge0tsms  47595  sge0rern  47603  sge0supre  47604  sge0le  47622  sge0fodjrnlem  47631  sge0rpcpnf  47636  meadjun  47677  meadjiunlem  47680  hoidmvlelem2  47811  hspdifhsp  47831  ovolval4lem1  47864  inlinecirc02plem  50103