MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.65da Structured version   Visualization version   GIF version

Theorem pm2.65da 600
Description: Deduction rule 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
StepHypRef Expression
1 pm2.65da.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 450 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 450 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 187 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  condan  835  nelrdva  3415  onnseq  7438  oeeulem  7678  disjen  8114  cantnflem1  8583  ssfin4  9129  fin1a2lem12  9230  fin1a2lem13  9231  canthnumlem  9467  canthwelem  9469  supaddc  10987  supmul1  10989  ixxdisj  12187  ixxub  12193  ixxlb  12194  icodisj  12294  discr1  12995  sqrlem7  13983  bitsfzolem  15150  bitsfzo  15151  sqnprm  15408  mreexexlem2d  16299  acsinfd  17174  lbsextlem3  19154  lbsextlem4  19155  iunconn  21225  dissnlocfin  21326  ptcmplem4  21853  iccntr  22618  evth  22752  bcthlem5  23119  ovolicopnf  23286  vitalilem4  23374  dvferm1  23742  dvferm2  23744  dgreq0  24015  radcnvle  24168  isosctrlem2  24543  dmlogdmgm  24744  mersenne  24946  pntlem3  25292  ostth2lem1  25301  tgbtwnne  25379  tglowdim1i  25390  tgbtwndiff  25395  tgbtwnconn1lem3  25463  legso  25488  tglineintmo  25531  tglineneq  25533  tglowdim2ln  25540  mirne  25556  mirhl  25568  krippenlem  25579  midexlem  25581  footex  25607  colperpexlem3  25618  mideulem2  25620  opphllem  25621  oppne3  25629  oppnid  25632  opphllem1  25633  opphllem2  25634  outpasch  25641  hlpasch  25642  hpgerlem  25651  colhp  25656  trgcopy  25690  cgrancol  25714  tgasa1  25733  umgrnloop2  26035  ex-natded5.5  27251  ex-natded5.8  27254  ex-natded5.13  27256  nn0min  29552  2sqn0  29631  ornglmullt  29792  orngrmullt  29793  qqhre  30049  esumcvgre  30138  carsgclctunlem2  30366  oddpwdc  30401  eulerpartlemf  30417  ballotlemfc0  30539  ballotlemfcc  30540  ballotlemimin  30552  ballotlem1c  30554  reprinfz1  30685  bnj1417  31094  unbdqndv2lem2  32485  knoppndvlem13  32499  topdifinffinlem  33175  poimirlem11  33400  poimirlem12  33401  imo72b2  38301  iunconnlem2  38997  n0p  39035  uzwo4  39047  ssnct  39075  nsstr  39099  disjrnmpt2  39197  difmap  39221  difmapsn  39226  mapssbi  39227  xrlexaddrp  39387  infleinflem2  39406  xrralrecnnge  39432  supminfxr2  39518  icoub  39561  ioonct  39573  ressioosup  39591  ressiooinf  39593  limclner  39689  limsupub  39742  climlimsupcex  39801  icccncfext  39869  fperdvper  39902  dvdivbd  39907  dvdsn1add  39923  dvmptfprodlem  39928  dvnprodlem3  39932  fourierdlem10  40103  fourierdlem19  40112  fourierdlem20  40113  fourierdlem35  40128  fourierdlem40  40133  fourierdlem41  40134  fourierdlem42  40135  fourierdlem46  40138  fourierdlem48  40140  fourierdlem49  40141  fourierdlem57  40149  fourierdlem58  40150  fourierdlem59  40151  fourierdlem63  40155  fourierdlem64  40156  fourierdlem65  40157  fourierdlem68  40160  fourierdlem74  40166  fourierdlem75  40167  fourierdlem78  40170  fourierdlem79  40171  fourierdlem80  40172  elaa2  40220  etransclem35  40255  etransclem38  40258  prsal  40307  fge0npnf  40353  sge0tsms  40366  sge0rern  40374  sge0supre  40375  sge0le  40393  sge0fodjrnlem  40402  sge0rpcpnf  40407  meadjun  40448  meadjiunlem  40451  hoidmvlelem2  40579  hspdifhsp  40599  ovolval4lem1  40632  preimagelt  40681  preimalegt  40682
  Copyright terms: Public domain W3C validator