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  4343  po3nr  4344  ordn2lp  4428  onssneli  4518  tfi  4660  nnlim  4685  smoord  6398  tz7.48-3  6472  oalimcl  6574  omlimcl  6592  oneo  6595  omopth2  6598  nnneo  6665  mapdom2  7048  php3  7063  onomeneq  7066  sucdom2  7073  isfinite2  7131  domunfican  7145  ordtypelem7  7255  unxpwdom2  7318  cantnfp1lem2  7397  cantnfp1lem3  7398  oemapvali  7402  cantnflem1  7407  cantnflem2  7408  rankpwi  7511  tskwe  7599  alephordi  7717  alephdom  7724  cardaleph  7732  cflim2  7905  isfin4-3  7957  fin23lem26  7967  fin1a2lem13  8054  axcclem  8099  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  pwfseqlem3  8298  pwxpndom2  8303  pwxpndom  8304  pwcdandom  8305  gchaleph  8313  r1wunlim  8375  inatsk  8416  tskuni  8421  gruina  8456  prlem934  8673  qextltlem  10545  ixxub  10693  ixxlb  10694  seqf1olem1  11101  facndiv  11317  hashbclem  11406  cnpart  11741  rlimuni  12040  rlimcld2  12068  isercoll  12157  sumrblem  12200  incexclem  12311  isumltss  12323  alzdvds  12594  fzm1ndvds  12596  fzo0dvdseq  12597  bitsfzolem  12641  smuval2  12689  smupvallem  12690  bezoutlem3  12735  rpdvds  12819  nonsq  12846  prmdiv  12869  odzdvds  12876  pcprendvds  12909  pcprendvds2  12910  pcpremul  12912  pcdvdsb  12937  pcadd2  12954  pockthlem  12968  prmreclem5  12983  prmreclem6  12984  1arith  12990  4sqlem11  13018  vdwlem11  13054  vdwlem12  13055  ramubcl  13081  ramub1lem2  13090  mrissmrcd  13558  pltnlt  14118  acsfiindd  14296  odcl2  14894  gexnnod  14915  pgpssslw  14941  torsubg  15162  lt6abl  15197  ablfacrplem  15316  pgpfac1lem3  15328  irredrmul  15505  lbspss  15851  islbs3  15924  lbsextlem3  15929  lbsextlem4  15930  mvrf1  16186  perfopn  16931  pnfnei  16966  mnfnei  16967  haust1  17096  cmpcld  17145  ptbasfi  17292  fbncp  17550  isfild  17569  fbasfip  17579  filufint  17631  rnelfmlem  17663  fmfnfm  17669  fclscf  17736  fclscmpi  17740  ptcmplem3  17764  opnsubg  17806  bldisj  17971  iccntr  18342  icccmplem2  18344  reconnlem1  18347  reconnlem2  18348  evth  18473  lebnumlem3  18477  ovolicc2lem3  18894  volfiniun  18920  iundisj  18921  dvne0  19374  lhop2  19378  lhop  19379  dvcnvrelem1  19380  itgsubstlem  19411  coemullem  19647  plyexmo  19709  wilthlem2  20323  wilth  20325  mumul  20435  chtublem  20466  perfect1  20483  lgsdilem2  20586  lgsne0  20588  lgsqrlem2  20597  lgseisenlem1  20604  lgseisenlem2  20605  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2lem1  20613  2sqblem  20632  chebbnd1lem1  20634  pntpbnd2  20752  pntlem3  20774  ostth  20804  chirredlem1  22986  iundisjfi  23378  iundisjf  23380  logccne0  23412  erdszelem8  23744  vdgr1a  23912  dedekind  24097  fundmpss  24193  dfon2lem4  24213  dfon2lem7  24216  sltval2  24381  sltasym  24397  axlowdimlem17  24658  broutsideof2  24817  outsidele  24827  onint1  24960  nn0prpwlem  26341  nn0prpw  26342  pellexlem6  27022  elpell14qr2  27050  pellfundglb  27073  jm2.19  27189  jm2.26lem3  27197  setindtr  27220  harinf  27230  lindfrn  27394  f1lindf  27395  dgraa0p  27457  lpssat  29825  exatleN  30215  3noncolr2  30260  4noncolr3  30264  3dimlem3  30272  3dimlem3OLDN  30273  3dimlem4a  30274  3dimlem4  30275  3dimlem4OLDN  30276  3atlem4  30297  3atlem5  30298  3atlem6  30299  llnnleat  30324  lplnnle2at  30352  lvolnle3at  30393  4atlem0a  30404  4atlem0ae  30405  dalem21  30505  dalem54  30537  cdlemblem  30604  osumcllem10N  30776  pexmidlem7N  30787  lhpmcvr4N  30837  4atexlemnclw  30881  cdlemd3  31011  cdleme3g  31045  cdleme3h  31046  cdleme7aa  31053  cdleme7d  31057  cdleme7ga  31059  cdleme11c  31072  cdleme15b  31086  cdleme20zN  31112  cdleme20y  31113  cdleme21b  31137  cdleme21c  31138  cdleme21ct  31140  cdleme22b  31152  cdleme32b  31253  cdleme35fnpq  31260  cdleme35f  31265  cdleme36a  31271  cdleme42c  31283  cdleme48bw  31313  cdlemf1  31372  cdlemg2fv2  31411  cdlemg7fvbwN  31418  cdlemg4  31428  cdlemg6c  31431  cdlemg27a  31503  cdlemg27b  31507  cdlemk3  31644  dia2dimlem1  31876  dihord6apre  32068  dihord6b  32072  dihord5apre  32074  dihglbcpreN  32112  dihmeetlem6  32121  dochnel2  32204  dochexmidlem7  32278  mapdindp2  32533  mapdindp3  32534  lspindp5  32582  mapdh8b  32592  hdmapval3lemN  32652  hdmap11lem1  32656  hdmapip0  32730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator