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 800
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 397 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 397 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 187 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 383
This theorem is referenced by:  condan  801  nelrdva  3567  onnseq  7593  oeeulem  7834  disjen  8272  cantnflem1  8749  ssfin4  9333  fin1a2lem12  9434  fin1a2lem13  9435  canthnumlem  9671  canthwelem  9673  supaddc  11191  supmul1  11193  ixxdisj  12394  ixxub  12400  ixxlb  12401  icodisj  12503  discr1  13206  sqrlem7  14196  bitsfzolem  15363  bitsfzo  15364  sqnprm  15620  mreexexlem2d  16512  acsinfd  17387  lbsextlem3  19374  lbsextlem4  19375  iunconn  21451  dissnlocfin  21552  ptcmplem4  22078  iccntr  22843  evth  22977  bcthlem5  23343  ovolicopnf  23511  vitalilem4  23598  dvferm1  23967  dvferm2  23969  dgreq0  24240  radcnvle  24393  isosctrlem2  24769  dmlogdmgm  24970  mersenne  25172  pntlem3  25518  ostth2lem1  25527  tgbtwnne  25605  tglowdim1i  25616  tgbtwndiff  25621  tgbtwnconn1lem3  25689  legso  25714  tglineintmo  25757  tglineneq  25759  tglowdim2ln  25766  mirne  25782  mirhl  25794  krippenlem  25805  midexlem  25807  footex  25833  colperpexlem3  25844  mideulem2  25846  opphllem  25847  oppne3  25855  oppnid  25858  opphllem1  25859  opphllem2  25860  outpasch  25867  hlpasch  25868  hpgerlem  25877  colhp  25882  trgcopy  25916  cgrancol  25940  tgasa1  25959  umgrnloop2  26262  ex-natded5.5  27603  ex-natded5.8  27606  ex-natded5.13  27608  nn0min  29901  2sqn0  29980  ornglmullt  30141  orngrmullt  30142  qqhre  30398  esumcvgre  30487  carsgclctunlem2  30715  oddpwdc  30750  eulerpartlemf  30766  ballotlemfc0  30888  ballotlemfcc  30889  ballotlemimin  30901  ballotlem1c  30903  reprinfz1  31034  bnj1417  31441  unbdqndv2lem2  32832  knoppndvlem13  32846  topdifinffinlem  33525  poimirlem11  33746  poimirlem12  33747  imo72b2  38994  iunconnlem2  39687  n0p  39724  uzwo4  39736  ssnct  39764  nsstr  39788  disjrnmpt2  39889  difmap  39911  difmapsn  39916  mapssbi  39917  xrlexaddrp  40078  infleinflem2  40097  xrralrecnnge  40123  supminfxr2  40209  xrpnf  40226  icoub  40265  ioonct  40276  ressioosup  40294  ressiooinf  40296  limclner  40395  limsupub  40448  climxrrelem  40493  climlimsupcex  40513  icccncfext  40612  fperdvper  40645  dvdivbd  40650  dvdsn1add  40666  dvmptfprodlem  40671  dvnprodlem3  40675  fourierdlem10  40845  fourierdlem19  40854  fourierdlem20  40855  fourierdlem35  40870  fourierdlem40  40875  fourierdlem41  40876  fourierdlem42  40877  fourierdlem46  40880  fourierdlem48  40882  fourierdlem49  40883  fourierdlem57  40891  fourierdlem58  40892  fourierdlem59  40893  fourierdlem63  40897  fourierdlem64  40898  fourierdlem65  40899  fourierdlem68  40902  fourierdlem74  40908  fourierdlem75  40909  fourierdlem78  40912  fourierdlem79  40913  fourierdlem80  40914  elaa2  40962  etransclem35  40997  etransclem38  41000  prsal  41049  fge0npnf  41095  sge0tsms  41108  sge0rern  41116  sge0supre  41117  sge0le  41135  sge0fodjrnlem  41144  sge0rpcpnf  41149  meadjun  41190  meadjiunlem  41193  hoidmvlelem2  41324  hspdifhsp  41344  ovolval4lem1  41377  preimagelt  41426  preimalegt  41427
  Copyright terms: Public domain W3C validator