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 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
StepHypRef Expression
1 pm2.65da.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 413 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 413 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 195 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  condan  816  nelrdva  3661  eqsnuniex  5314  onnseq  8282  oeeulem  8540  disjen  9036  cantnflem1  9583  ssfin4  10204  fin1a2lem12  10305  fin1a2lem13  10306  canthnumlem  10542  canthwelem  10544  supaddc  12080  supmul1  12082  ixxdisj  13233  ixxub  13239  ixxlb  13240  icodisj  13347  discr1  14096  01sqrexlem7  15093  bitsfzolem  16274  bitsfzo  16275  sqnprm  16538  mreexexlem2d  17485  acsinfd  18405  simpgntrivd  19836  prmgrpsimpgd  19852  ablsimpgprmd  19853  lbsextlem3  20574  lbsextlem4  20575  iunconn  22731  dissnlocfin  22832  ptcmplem4  23358  iccntr  24136  evth  24274  bcthlem5  24644  ovolicopnf  24840  vitalilem4  24927  dvferm1  25301  dvferm2  25303  dgreq0  25578  radcnvle  25731  isosctrlem2  26121  dmlogdmgm  26325  mersenne  26527  2sqn0  26734  pntlem3  26909  ostth2lem1  26918  tgbtwnne  27261  tglowdim1i  27272  tgbtwndiff  27277  tgbtwnconn1lem3  27345  legso  27370  tglineintmo  27413  tglineneq  27415  tglowdim2ln  27422  mirne  27438  mirhl  27450  krippenlem  27461  midexlem  27463  footexALT  27489  footexlem2  27491  colperpexlem3  27503  mideulem2  27505  opphllem  27506  oppnid  27517  opphllem2  27519  outpasch  27526  hlpasch  27527  hpgerlem  27536  colhp  27541  trgcopy  27575  tgasa1  27629  umgrnloop2  27926  ex-natded5.5  29183  ex-natded5.8  29186  ex-natded5.13  29188  unidifsnne  31292  nn0min  31542  ornglmullt  31928  orngrmullt  31929  0nellinds  31985  pidlnz  31990  0ringprmidl  32044  qsidomlem1  32047  krull  32062  0ringmon1p  32086  lvecdim0  32124  lindsunlem  32139  zarcls1  32262  zarclsint  32265  qqhre  32413  esumcvgre  32502  carsgclctunlem2  32731  oddpwdc  32766  eulerpartlemf  32782  ballotlemfc0  32904  ballotlemfcc  32905  ballotlemimin  32917  ballotlem1c  32919  reprinfz1  33047  bnj1417  33465  unbdqndv2lem2  34911  knoppndvlem13  34925  irrdiff  35735  topdifinffinlem  35756  pibt2  35826  poimirlem11  36027  poimirlem12  36028  aks4d1p7  40478  aks4d1p8d2  40480  aks4d1p8  40482  aks4d1p9  40483  fldhmf1  40485  imo72b2  42356  iunconnlem2  43128  n0p  43162  uzwo4  43172  ssnct  43198  nsstr  43216  disjrnmpt2  43312  difmap  43333  difmapsn  43338  mapssbi  43339  xrlexaddrp  43491  infleinflem2  43510  xrralrecnnge  43530  supminfxr2  43609  xrpnf  43626  icoub  43665  ioonct  43676  ressioosup  43694  ressiooinf  43696  limclner  43793  limsupub  43846  climxrrelem  43891  climlimsupcex  43911  icccncfext  44029  fperdvper  44061  dvdivbd  44065  dvdsn1add  44081  dvmptfprodlem  44086  dvnprodlem3  44090  fourierdlem10  44259  fourierdlem19  44268  fourierdlem20  44269  fourierdlem35  44284  fourierdlem40  44289  fourierdlem41  44290  fourierdlem42  44291  fourierdlem46  44294  fourierdlem48  44296  fourierdlem49  44297  fourierdlem57  44305  fourierdlem58  44306  fourierdlem59  44307  fourierdlem63  44311  fourierdlem64  44312  fourierdlem65  44313  fourierdlem68  44316  fourierdlem74  44322  fourierdlem75  44323  fourierdlem78  44326  fourierdlem79  44327  fourierdlem80  44328  elaa2  44376  etransclem35  44411  etransclem38  44414  fge0npnf  44509  sge0tsms  44522  sge0rern  44530  sge0supre  44531  sge0le  44549  sge0fodjrnlem  44558  sge0rpcpnf  44563  meadjun  44604  meadjiunlem  44607  hoidmvlelem2  44738  hspdifhsp  44758  ovolval4lem1  44791
  Copyright terms: Public domain W3C validator