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 415 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 415 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 198 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  condan  816  nelrdva  3694  onnseq  7973  oeeulem  8219  disjen  8666  cantnflem1  9144  ssfin4  9724  fin1a2lem12  9825  fin1a2lem13  9826  canthnumlem  10062  canthwelem  10064  supaddc  11600  supmul1  11602  ixxdisj  12745  ixxub  12751  ixxlb  12752  icodisj  12854  discr1  13592  sqrlem7  14600  bitsfzolem  15775  bitsfzo  15776  sqnprm  16038  mreexexlem2d  16908  acsinfd  17782  simpgntrivd  19212  prmgrpsimpgd  19228  ablsimpgprmd  19229  lbsextlem3  19924  lbsextlem4  19925  iunconn  22028  dissnlocfin  22129  ptcmplem4  22655  iccntr  23421  evth  23555  bcthlem5  23923  ovolicopnf  24117  vitalilem4  24204  dvferm1  24574  dvferm2  24576  dgreq0  24847  radcnvle  25000  isosctrlem2  25389  dmlogdmgm  25593  mersenne  25795  2sqn0  26002  pntlem3  26177  ostth2lem1  26186  tgbtwnne  26268  tglowdim1i  26279  tgbtwndiff  26284  tgbtwnconn1lem3  26352  legso  26377  tglineintmo  26420  tglineneq  26422  tglowdim2ln  26429  mirne  26445  mirhl  26457  krippenlem  26468  midexlem  26470  footexALT  26496  footexlem2  26498  colperpexlem3  26510  mideulem2  26512  opphllem  26513  oppnid  26524  opphllem2  26526  outpasch  26533  hlpasch  26534  hpgerlem  26543  colhp  26548  trgcopy  26582  tgasa1  26636  umgrnloop2  26923  ex-natded5.5  28181  ex-natded5.8  28184  ex-natded5.13  28186  unidifsnne  30288  nn0min  30529  ornglmullt  30873  orngrmullt  30874  0nellinds  30928  qsidomlem1  30957  lvecdim0  30993  lindsunlem  31008  qqhre  31249  esumcvgre  31338  carsgclctunlem2  31565  oddpwdc  31600  eulerpartlemf  31616  ballotlemfc0  31738  ballotlemfcc  31739  ballotlemimin  31751  ballotlem1c  31753  reprinfz1  31881  bnj1417  32301  unbdqndv2lem2  33837  knoppndvlem13  33851  topdifinffinlem  34615  pibt2  34685  poimirlem11  34890  poimirlem12  34891  imo72b2  40510  iunconnlem2  41254  n0p  41290  uzwo4  41300  ssnct  41326  nsstr  41346  disjrnmpt2  41433  difmap  41454  difmapsn  41459  mapssbi  41460  xrlexaddrp  41604  infleinflem2  41623  xrralrecnnge  41646  supminfxr2  41729  xrpnf  41746  icoub  41786  ioonct  41797  ressioosup  41815  ressiooinf  41817  limclner  41916  limsupub  41969  climxrrelem  42014  climlimsupcex  42034  icccncfext  42154  fperdvper  42187  dvdivbd  42192  dvdsn1add  42208  dvmptfprodlem  42213  dvnprodlem3  42217  fourierdlem10  42387  fourierdlem19  42396  fourierdlem20  42397  fourierdlem35  42412  fourierdlem40  42417  fourierdlem41  42418  fourierdlem42  42419  fourierdlem46  42422  fourierdlem48  42424  fourierdlem49  42425  fourierdlem57  42433  fourierdlem58  42434  fourierdlem59  42435  fourierdlem63  42439  fourierdlem64  42440  fourierdlem65  42441  fourierdlem68  42444  fourierdlem74  42450  fourierdlem75  42451  fourierdlem78  42454  fourierdlem79  42455  fourierdlem80  42456  elaa2  42504  etransclem35  42539  etransclem38  42542  fge0npnf  42634  sge0tsms  42647  sge0rern  42655  sge0supre  42656  sge0le  42674  sge0fodjrnlem  42683  sge0rpcpnf  42688  meadjun  42729  meadjiunlem  42732  hoidmvlelem2  42863  hspdifhsp  42883  ovolval4lem1  42916
  Copyright terms: Public domain W3C validator