Theorem pm2.65da 815

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  condan  816  nelrdva  3698  onnseq  7983  oeeulem  8229  disjen  8676  cantnflem1  9154  ssfin4  9734  fin1a2lem12  9835  fin1a2lem13  9836  canthnumlem  10072  canthwelem  10074  supaddc  11610  supmul1  11612  ixxdisj  12756  ixxub  12762  ixxlb  12763  icodisj  12865  discr1  13603  sqrlem7  14610  bitsfzolem  15785  bitsfzo  15786  sqnprm  16048  mreexexlem2d  16918  acsinfd  17792  simpgntrivd  19222  prmgrpsimpgd  19238  ablsimpgprmd  19239  lbsextlem3  19934  lbsextlem4  19935  iunconn  22038  dissnlocfin  22139  ptcmplem4  22665  iccntr  23431  evth  23565  bcthlem5  23933  ovolicopnf  24127  vitalilem4  24214  dvferm1  24584  dvferm2  24586  dgreq0  24857  radcnvle  25010  isosctrlem2  25399  dmlogdmgm  25603  mersenne  25805  2sqn0  26012  pntlem3  26187  ostth2lem1  26196  tgbtwnne  26278  tglowdim1i  26289  tgbtwndiff  26294  tgbtwnconn1lem3  26362  legso  26387  tglineintmo  26430  tglineneq  26432  tglowdim2ln  26439  mirne  26455  mirhl  26467  krippenlem  26478  midexlem  26480  footexALT  26506  footexlem2  26508  colperpexlem3  26520  mideulem2  26522  opphllem  26523  oppnid  26534  opphllem2  26536  outpasch  26543  hlpasch  26544  hpgerlem  26553  colhp  26558  trgcopy  26592  tgasa1  26646  umgrnloop2  26933  ex-natded5.5  28191  ex-natded5.8  28194  ex-natded5.13  28196  unidifsnne  30298  nn0min  30538  ornglmullt  30882  orngrmullt  30883  0nellinds  30937  qsidomlem1  30967  krull  30982  lvecdim0  31007  lindsunlem  31022  qqhre  31263  esumcvgre  31352  carsgclctunlem2  31579  oddpwdc  31614  eulerpartlemf  31630  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemimin  31765  ballotlem1c  31767  reprinfz1  31895  bnj1417  32315  unbdqndv2lem2  33851  knoppndvlem13  33865  topdifinffinlem  34630  pibt2  34700  poimirlem11  34905  poimirlem12  34906  imo72b2  40532  iunconnlem2  41276  n0p  41312  uzwo4  41322  ssnct  41348  nsstr  41368  disjrnmpt2  41456  difmap  41477  difmapsn  41482  mapssbi  41483  xrlexaddrp  41627  infleinflem2  41646  xrralrecnnge  41669  supminfxr2  41752  xrpnf  41769  icoub  41809  ioonct  41820  ressioosup  41838  ressiooinf  41840  limclner  41939  limsupub  41992  climxrrelem  42037  climlimsupcex  42057  icccncfext  42177  fperdvper  42210  dvdivbd  42215  dvdsn1add  42231  dvmptfprodlem  42236  dvnprodlem3  42240  fourierdlem10  42409  fourierdlem19  42418  fourierdlem20  42419  fourierdlem35  42434  fourierdlem40  42439  fourierdlem41  42440  fourierdlem42  42441  fourierdlem46  42444  fourierdlem48  42446  fourierdlem49  42447  fourierdlem57  42455  fourierdlem58  42456  fourierdlem59  42457  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem68  42466  fourierdlem74  42472  fourierdlem75  42473  fourierdlem78  42476  fourierdlem79  42477  fourierdlem80  42478  elaa2  42526  etransclem35  42561  etransclem38  42564  fge0npnf  42656  sge0tsms  42669  sge0rern  42677  sge0supre  42678  sge0le  42696  sge0fodjrnlem  42705  sge0rpcpnf  42710  meadjun  42751  meadjiunlem  42754  hoidmvlelem2  42885  hspdifhsp  42905  ovolval4lem1  42938