MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtod Unicode version

Theorem mtod 168
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1  |-  ( ph  ->  -.  ch )
mtod.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mtod  |-  ( ph  ->  -.  ps )

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 mtod.1 . . 3  |-  ( ph  ->  -.  ch )
32a1d 22 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
41, 3pm2.65d 166 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mtoi  169  mtbid  291  mtbird  292  mtand  640  mtord  641  po2nr  4327  po3nr  4328  ordn2lp  4412  onssneli  4502  tfi  4644  nnlim  4669  smoord  6382  tz7.48-3  6456  oalimcl  6558  omlimcl  6576  oneo  6579  omopth2  6582  nnneo  6649  mapdom2  7032  php3  7047  onomeneq  7050  sucdom2  7057  isfinite2  7115  domunfican  7129  ordtypelem7  7239  unxpwdom2  7302  cantnfp1lem2  7381  cantnfp1lem3  7382  oemapvali  7386  cantnflem1  7391  cantnflem2  7392  rankpwi  7495  tskwe  7583  alephordi  7701  alephdom  7708  cardaleph  7716  cflim2  7889  isfin4-3  7941  fin23lem26  7951  fin1a2lem13  8038  axcclem  8083  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  pwfseqlem3  8282  pwxpndom2  8287  pwxpndom  8288  pwcdandom  8289  gchaleph  8297  r1wunlim  8359  inatsk  8400  tskuni  8405  gruina  8440  prlem934  8657  qextltlem  10529  ixxub  10677  ixxlb  10678  seqf1olem1  11085  facndiv  11301  hashbclem  11390  cnpart  11725  rlimuni  12024  rlimcld2  12052  isercoll  12141  sumrblem  12184  incexclem  12295  isumltss  12307  alzdvds  12578  fzm1ndvds  12580  fzo0dvdseq  12581  bitsfzolem  12625  smuval2  12673  smupvallem  12674  bezoutlem3  12719  rpdvds  12803  nonsq  12830  prmdiv  12853  odzdvds  12860  pcprendvds  12893  pcprendvds2  12894  pcpremul  12896  pcdvdsb  12921  pcadd2  12938  pockthlem  12952  prmreclem5  12967  prmreclem6  12968  1arith  12974  4sqlem11  13002  vdwlem11  13038  vdwlem12  13039  ramubcl  13065  ramub1lem2  13074  mrissmrcd  13542  pltnlt  14102  acsfiindd  14280  odcl2  14878  gexnnod  14899  pgpssslw  14925  torsubg  15146  lt6abl  15181  ablfacrplem  15300  pgpfac1lem3  15312  irredrmul  15489  lbspss  15835  islbs3  15908  lbsextlem3  15913  lbsextlem4  15914  mvrf1  16170  perfopn  16915  pnfnei  16950  mnfnei  16951  haust1  17080  cmpcld  17129  ptbasfi  17276  fbncp  17534  isfild  17553  fbasfip  17563  filufint  17615  rnelfmlem  17647  fmfnfm  17653  fclscf  17720  fclscmpi  17724  ptcmplem3  17748  opnsubg  17790  bldisj  17955  iccntr  18326  icccmplem2  18328  reconnlem1  18331  reconnlem2  18332  evth  18457  lebnumlem3  18461  ovolicc2lem3  18878  volfiniun  18904  iundisj  18905  dvne0  19358  lhop2  19362  lhop  19363  dvcnvrelem1  19364  itgsubstlem  19395  coemullem  19631  plyexmo  19693  wilthlem2  20307  wilth  20309  mumul  20419  chtublem  20450  perfect1  20467  lgsdilem2  20570  lgsne0  20572  lgsqrlem2  20581  lgseisenlem1  20588  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2lem1  20597  2sqblem  20616  chebbnd1lem1  20618  pntpbnd2  20736  pntlem3  20758  ostth  20788  chirredlem1  22970  iundisjfi  23363  iundisjf  23365  logccne0  23397  erdszelem8  23729  vdgr1a  23897  dedekind  24082  fundmpss  24122  dfon2lem4  24142  dfon2lem7  24145  sltval2  24310  sltasym  24326  axlowdimlem17  24586  broutsideof2  24745  outsidele  24755  onint1  24888  nn0prpwlem  26238  nn0prpw  26239  pellexlem6  26919  elpell14qr2  26947  pellfundglb  26970  jm2.19  27086  jm2.26lem3  27094  setindtr  27117  harinf  27127  lindfrn  27291  f1lindf  27292  dgraa0p  27354  lpssat  29203  exatleN  29593  3noncolr2  29638  4noncolr3  29642  3dimlem3  29650  3dimlem3OLDN  29651  3dimlem4a  29652  3dimlem4  29653  3dimlem4OLDN  29654  3atlem4  29675  3atlem5  29676  3atlem6  29677  llnnleat  29702  lplnnle2at  29730  lvolnle3at  29771  4atlem0a  29782  4atlem0ae  29783  dalem21  29883  dalem54  29915  cdlemblem  29982  osumcllem10N  30154  pexmidlem7N  30165  lhpmcvr4N  30215  4atexlemnclw  30259  cdlemd3  30389  cdleme3g  30423  cdleme3h  30424  cdleme7aa  30431  cdleme7d  30435  cdleme7ga  30437  cdleme11c  30450  cdleme15b  30464  cdleme20zN  30490  cdleme20y  30491  cdleme21b  30515  cdleme21c  30516  cdleme21ct  30518  cdleme22b  30530  cdleme32b  30631  cdleme35fnpq  30638  cdleme35f  30643  cdleme36a  30649  cdleme42c  30661  cdleme48bw  30691  cdlemf1  30750  cdlemg2fv2  30789  cdlemg7fvbwN  30796  cdlemg4  30806  cdlemg6c  30809  cdlemg27a  30881  cdlemg27b  30885  cdlemk3  31022  dia2dimlem1  31254  dihord6apre  31446  dihord6b  31450  dihord5apre  31452  dihglbcpreN  31490  dihmeetlem6  31499  dochnel2  31582  dochexmidlem7  31656  mapdindp2  31911  mapdindp3  31912  lspindp5  31960  mapdh8b  31970  hdmapval3lemN  32030  hdmap11lem1  32034  hdmapip0  32108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator