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

Theorem pm2.65da 599
 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  834  nelrdva  3403  onnseq  7393  oeeulem  7633  disjen  8069  cantnflem1  8538  ssfin4  9084  fin1a2lem12  9185  fin1a2lem13  9186  canthnumlem  9422  canthwelem  9424  supaddc  10942  supmul1  10944  ixxdisj  12140  ixxub  12146  ixxlb  12147  icodisj  12247  discr1  12948  sqrlem7  13931  bitsfzolem  15091  bitsfzo  15092  sqnprm  15349  mreexexlem2d  16237  acsinfd  17112  lbsextlem3  19092  lbsextlem4  19093  iunconn  21154  dissnlocfin  21255  ptcmplem4  21782  iccntr  22547  evth  22681  bcthlem5  23048  ovolicopnf  23215  vitalilem4  23303  dvferm1  23669  dvferm2  23671  dgreq0  23942  radcnvle  24095  isosctrlem2  24466  dmlogdmgm  24667  mersenne  24869  pntlem3  25215  ostth2lem1  25224  tgbtwnne  25302  tglowdim1i  25313  tgbtwndiff  25318  tgbtwnconn1lem3  25386  legso  25411  tglineintmo  25454  tglineneq  25456  tglowdim2ln  25463  mirne  25479  mirhl  25491  krippenlem  25502  midexlem  25504  footex  25530  colperpexlem3  25541  mideulem2  25543  opphllem  25544  oppne3  25552  oppnid  25555  opphllem1  25556  opphllem2  25557  outpasch  25564  hlpasch  25565  hpgerlem  25574  colhp  25579  trgcopy  25613  cgrancol  25637  tgasa1  25656  umgrnloop2  25951  ex-natded5.5  27138  ex-natded5.8  27141  ex-natded5.13  27143  nn0min  29432  2sqn0  29455  ornglmullt  29616  orngrmullt  29617  qqhre  29870  esumcvgre  29958  carsgclctunlem2  30186  oddpwdc  30221  eulerpartlemf  30237  ballotlemfc0  30359  ballotlemfcc  30360  ballotlemimin  30372  ballotlem1c  30374  bnj1417  30852  unbdqndv2lem2  32178  knoppndvlem13  32192  topdifinffinlem  32862  poimirlem11  33087  poimirlem12  33088  imo72b2  37992  iunconnlem2  38689  n0p  38727  uzwo4  38739  ssnct  38767  nsstr  38791  disjrnmpt2  38880  difmap  38904  difmapsn  38909  mapssbi  38910  xrlexaddrp  39063  infleinflem2  39082  xrralrecnnge  39108  icoub  39194  ioonct  39206  ressioosup  39224  ressiooinf  39226  limclner  39315  limsupub  39368  icccncfext  39431  fperdvper  39466  dvdivbd  39471  dvdsn1add  39487  dvmptfprodlem  39492  dvnprodlem3  39496  fourierdlem10  39667  fourierdlem19  39676  fourierdlem20  39677  fourierdlem35  39692  fourierdlem40  39697  fourierdlem41  39698  fourierdlem42  39699  fourierdlem46  39702  fourierdlem48  39704  fourierdlem49  39705  fourierdlem57  39713  fourierdlem58  39714  fourierdlem59  39715  fourierdlem63  39719  fourierdlem64  39720  fourierdlem65  39721  fourierdlem68  39724  fourierdlem74  39730  fourierdlem75  39731  fourierdlem78  39734  fourierdlem79  39735  fourierdlem80  39736  elaa2  39784  etransclem35  39819  etransclem38  39822  prsal  39871  fge0npnf  39917  sge0tsms  39930  sge0rern  39938  sge0supre  39939  sge0le  39957  sge0fodjrnlem  39966  sge0rpcpnf  39971  meadjun  40012  meadjiunlem  40015  hoidmvlelem2  40143  hspdifhsp  40163  ovolval4lem1  40196  preimagelt  40245  preimalegt  40246
 Copyright terms: Public domain W3C validator