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 842
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 399 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 399 . 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 198  df-an 385
This theorem is referenced by:  condan  843  nelrdva  3609  onnseq  7671  oeeulem  7912  disjen  8350  cantnflem1  8827  ssfin4  9411  fin1a2lem12  9512  fin1a2lem13  9513  canthnumlem  9749  canthwelem  9751  supaddc  11269  supmul1  11271  ixxdisj  12402  ixxub  12408  ixxlb  12409  icodisj  12512  discr1  13217  sqrlem7  14206  bitsfzolem  15369  bitsfzo  15370  sqnprm  15625  mreexexlem2d  16504  acsinfd  17379  lbsextlem3  19363  lbsextlem4  19364  iunconn  21439  dissnlocfin  21540  ptcmplem4  22066  iccntr  22831  evth  22965  bcthlem5  23331  ovolicopnf  23499  vitalilem4  23586  dvferm1  23956  dvferm2  23958  dgreq0  24229  radcnvle  24382  isosctrlem2  24757  dmlogdmgm  24958  mersenne  25160  pntlem3  25506  ostth2lem1  25515  tgbtwnne  25593  tglowdim1i  25604  tgbtwndiff  25609  tgbtwnconn1lem3  25677  legso  25702  tglineintmo  25745  tglineneq  25747  tglowdim2ln  25754  mirne  25770  mirhl  25782  krippenlem  25793  midexlem  25795  footex  25821  colperpexlem3  25832  mideulem2  25834  opphllem  25835  oppne3  25843  oppnid  25846  opphllem1  25847  opphllem2  25848  outpasch  25855  hlpasch  25856  hpgerlem  25865  colhp  25870  trgcopy  25904  cgrancol  25928  tgasa1  25947  umgrnloop2  26250  ex-natded5.5  27592  ex-natded5.8  27595  ex-natded5.13  27597  nn0min  29888  2sqn0  29965  ornglmullt  30126  orngrmullt  30127  qqhre  30383  esumcvgre  30472  carsgclctunlem2  30700  oddpwdc  30735  eulerpartlemf  30751  ballotlemfc0  30873  ballotlemfcc  30874  ballotlemimin  30886  ballotlem1c  30888  reprinfz1  31019  bnj1417  31426  unbdqndv2lem2  32812  knoppndvlem13  32826  topdifinffinlem  33505  poimirlem11  33727  poimirlem12  33728  imo72b2  38969  iunconnlem2  39659  n0p  39696  uzwo4  39708  ssnct  39736  nsstr  39760  disjrnmpt2  39858  difmap  39880  difmapsn  39885  mapssbi  39886  xrlexaddrp  40042  infleinflem2  40061  xrralrecnnge  40086  supminfxr2  40172  xrpnf  40189  icoub  40227  ioonct  40238  ressioosup  40256  ressiooinf  40258  limclner  40357  limsupub  40410  climxrrelem  40455  climlimsupcex  40475  icccncfext  40574  fperdvper  40607  dvdivbd  40612  dvdsn1add  40628  dvmptfprodlem  40633  dvnprodlem3  40637  fourierdlem10  40807  fourierdlem19  40816  fourierdlem20  40817  fourierdlem35  40832  fourierdlem40  40837  fourierdlem41  40838  fourierdlem42  40839  fourierdlem46  40842  fourierdlem48  40844  fourierdlem49  40845  fourierdlem57  40853  fourierdlem58  40854  fourierdlem59  40855  fourierdlem63  40859  fourierdlem64  40860  fourierdlem65  40861  fourierdlem68  40864  fourierdlem74  40870  fourierdlem75  40871  fourierdlem78  40874  fourierdlem79  40875  fourierdlem80  40876  elaa2  40924  etransclem35  40959  etransclem38  40962  prsal  41011  fge0npnf  41057  sge0tsms  41070  sge0rern  41078  sge0supre  41079  sge0le  41097  sge0fodjrnlem  41106  sge0rpcpnf  41111  meadjun  41152  meadjiunlem  41155  hoidmvlelem2  41286  hspdifhsp  41306  ovolval4lem1  41339  preimagelt  41388  preimalegt  41389
  Copyright terms: Public domain W3C validator