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  3679  eqsnuniex  5319  onnseq  8316  oeeulem  8568  disjen  9104  cantnflem1  9649  ssfin4  10270  fin1a2lem12  10371  fin1a2lem13  10372  canthnumlem  10608  canthwelem  10610  supaddc  12157  supmul1  12159  ixxdisj  13328  ixxub  13334  ixxlb  13335  icodisj  13444  discr1  14211  01sqrexlem7  15221  bitsfzolem  16411  bitsfzo  16412  sqnprm  16679  mreexexlem2d  17613  acsinfd  18522  simpgntrivd  20037  prmgrpsimpgd  20053  ablsimpgprmd  20054  lbsextlem3  21077  lbsextlem4  21078  iunconn  23322  dissnlocfin  23423  ptcmplem4  23949  iccntr  24717  evth  24865  bcthlem5  25235  ovolicopnf  25432  vitalilem4  25519  dvferm1  25896  dvferm2  25898  dgreq0  26178  radcnvle  26336  isosctrlem2  26736  dmlogdmgm  26941  mersenne  27145  2sqn0  27352  pntlem3  27527  ostth2lem1  27536  tgbtwnne  28424  tglowdim1i  28435  tgbtwndiff  28440  tgbtwnconn1lem3  28508  legso  28533  tglineintmo  28576  tglineneq  28578  tglowdim2ln  28585  mirne  28601  mirhl  28613  krippenlem  28624  midexlem  28626  footexALT  28652  footexlem2  28654  colperpexlem3  28666  mideulem2  28668  opphllem  28669  oppnid  28680  opphllem2  28682  outpasch  28689  hlpasch  28690  hpgerlem  28699  colhp  28704  trgcopy  28738  tgasa1  28792  umgrnloop2  29080  ex-natded5.5  30346  ex-natded5.8  30349  ex-natded5.13  30351  unidifsnne  32472  ifnefals  32484  rexmul2  32684  hashpss  32741  nn0min  32752  ccatws1f1o  32880  elrgspnlem2  33201  fracfld  33265  ornglmullt  33292  orngrmullt  33293  0nellinds  33348  pidlnz  33354  drngidl  33411  drngidlhash  33412  0ringprmidl  33427  qsidomlem1  33430  mxidlirredi  33449  krull  33457  qsdrngi  33473  qsdrng  33475  rsprprmprmidlb  33501  rprmasso2  33504  1arithidom  33515  pidufd  33521  1arithufdlem3  33524  dfufd2  33528  0ringmon1p  33533  ig1pnunit  33573  exsslsb  33599  lvecdim0  33609  lindsunlem  33627  assafld  33640  fldextrspundgdvdslem  33682  irredminply  33713  constrextdg2lem  33745  constrext2chnlem  33747  2sqr3nconstr  33778  cos9thpinconstrlem2  33787  zarcls1  33866  zarclsint  33869  qqhre  34017  esumcvgre  34088  carsgclctunlem2  34317  oddpwdc  34352  eulerpartlemf  34368  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemimin  34504  ballotlem1c  34506  reprinfz1  34620  bnj1417  35038  unbdqndv2lem2  36505  knoppndvlem13  36519  irrdiff  37321  topdifinffinlem  37342  pibt2  37412  poimirlem11  37632  poimirlem12  37633  aks4d1p7  42078  aks4d1p8d2  42080  aks4d1p8  42082  aks4d1p9  42083  fldhmf1  42085  hashscontpow1  42116  aks6d1c5  42134  imo72b2  44168  iunconnlem2  44931  n0p  45046  uzwo4  45054  ssnct  45078  nsstr  45096  disjrnmpt2  45189  difmap  45208  difmapsn  45213  mapssbi  45214  xrlexaddrp  45355  infleinflem2  45374  xrralrecnnge  45393  supminfxr2  45472  xrpnf  45488  icoub  45531  ioonct  45542  ressioosup  45560  ressiooinf  45562  limclner  45656  limsupub  45709  climxrrelem  45754  climlimsupcex  45774  icccncfext  45892  fperdvper  45924  dvdivbd  45928  dvdsn1add  45944  dvmptfprodlem  45949  dvnprodlem3  45953  fourierdlem10  46122  fourierdlem19  46131  fourierdlem20  46132  fourierdlem35  46147  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem68  46179  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem79  46190  fourierdlem80  46191  elaa2  46239  etransclem35  46274  etransclem38  46277  fge0npnf  46372  sge0tsms  46385  sge0rern  46393  sge0supre  46394  sge0le  46412  sge0fodjrnlem  46421  sge0rpcpnf  46426  meadjun  46467  meadjiunlem  46470  hoidmvlelem2  46601  hspdifhsp  46621  ovolval4lem1  46654