Theorem pm2.65da 853

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

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

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 199  df-an 387

This theorem is referenced by:  condan  854  nelrdva  3644  onnseq  7707  oeeulem  7948  disjen  8386  cantnflem1  8863  ssfin4  9447  fin1a2lem12  9548  fin1a2lem13  9549  canthnumlem  9785  canthwelem  9787  supaddc  11320  supmul1  11322  ixxdisj  12478  ixxub  12484  ixxlb  12485  icodisj  12588  discr1  13294  sqrlem7  14366  bitsfzolem  15529  bitsfzo  15530  sqnprm  15785  mreexexlem2d  16658  acsinfd  17533  lbsextlem3  19521  lbsextlem4  19522  iunconn  21602  dissnlocfin  21703  ptcmplem4  22229  iccntr  22994  evth  23128  bcthlem5  23496  ovolicopnf  23690  vitalilem4  23777  dvferm1  24147  dvferm2  24149  dgreq0  24420  radcnvle  24573  isosctrlem2  24959  dmlogdmgm  25163  mersenne  25365  pntlem3  25711  ostth2lem1  25720  tgbtwnne  25802  tglowdim1i  25813  tgbtwndiff  25818  tgbtwnconn1lem3  25886  legso  25911  tglineintmo  25954  tglineneq  25956  tglowdim2ln  25963  mirne  25979  mirhl  25991  krippenlem  26002  midexlem  26004  footex  26030  colperpexlem3  26041  mideulem2  26043  opphllem  26044  oppne3  26052  oppnid  26055  opphllem1  26056  opphllem2  26057  outpasch  26064  hlpasch  26065  hpgerlem  26074  colhp  26079  trgcopy  26113  cgrancol  26137  tgasa1  26157  umgrnloop2  26445  ex-natded5.5  27825  ex-natded5.8  27828  ex-natded5.13  27830  nn0min  30114  2sqn0  30191  ornglmullt  30352  orngrmullt  30353  qqhre  30609  esumcvgre  30698  carsgclctunlem2  30926  oddpwdc  30961  eulerpartlemf  30977  ballotlemfc0  31100  ballotlemfcc  31101  ballotlemimin  31113  ballotlem1c  31115  reprinfz1  31249  bnj1417  31655  unbdqndv2lem2  33033  knoppndvlem13  33047  topdifinffinlem  33740  poimirlem11  33964  poimirlem12  33965  imo72b2  39315  iunconnlem2  39989  n0p  40026  uzwo4  40038  ssnct  40066  nsstr  40090  disjrnmpt2  40183  difmap  40205  difmapsn  40210  mapssbi  40211  xrlexaddrp  40365  infleinflem2  40384  xrralrecnnge  40408  supminfxr2  40493  xrpnf  40510  icoub  40548  ioonct  40559  ressioosup  40577  ressiooinf  40579  limclner  40678  limsupub  40731  climxrrelem  40776  climlimsupcex  40796  icccncfext  40895  fperdvper  40928  dvdivbd  40933  dvdsn1add  40949  dvmptfprodlem  40954  dvnprodlem3  40958  fourierdlem10  41128  fourierdlem19  41137  fourierdlem20  41138  fourierdlem35  41153  fourierdlem40  41158  fourierdlem41  41159  fourierdlem42  41160  fourierdlem46  41163  fourierdlem48  41165  fourierdlem49  41166  fourierdlem57  41174  fourierdlem58  41175  fourierdlem59  41176  fourierdlem63  41180  fourierdlem64  41181  fourierdlem65  41182  fourierdlem68  41185  fourierdlem74  41191  fourierdlem75  41192  fourierdlem78  41195  fourierdlem79  41196  fourierdlem80  41197  elaa2  41245  etransclem35  41280  etransclem38  41283  prsal  41329  fge0npnf  41375  sge0tsms  41388  sge0rern  41396  sge0supre  41397  sge0le  41415  sge0fodjrnlem  41424  sge0rpcpnf  41429  meadjun  41470  meadjiunlem  41473  hoidmvlelem2  41604  hspdifhsp  41624  ovolval4lem1  41657  preimagelt  41706  preimalegt  41707