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

Theorem mtod 171
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 24 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
41, 3pm2.65d 169 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mtoi  172  mtbid  293  mtbird  294  mtand  642  mtord  643  po2nr  4519  po3nr  4520  ordn2lp  4604  onssneli  4694  tfi  4836  nnlim  4861  smoord  6630  tz7.48-3  6704  oalimcl  6806  omlimcl  6824  oneo  6827  omopth2  6830  nnneo  6897  mapdom2  7281  php3  7296  onomeneq  7299  sucdom2  7306  isfinite2  7368  domunfican  7382  ordtypelem7  7496  unxpwdom2  7559  cantnfp1lem2  7638  oemapvali  7643  cantnflem1  7648  cantnflem2  7649  rankpwi  7752  tskwe  7842  alephordi  7960  alephdom  7967  cardaleph  7975  cflim2  8148  isfin4-3  8200  fin23lem26  8210  fin1a2lem13  8297  axcclem  8342  fpwwe2lem12  8521  fpwwe2lem13  8522  fpwwe2  8523  pwxpndom2  8545  pwxpndom  8546  pwcdandom  8547  gchaleph  8551  r1wunlim  8617  inatsk  8658  tskuni  8663  gruina  8698  prlem934  8915  qextltlem  10793  ixxub  10942  ixxlb  10943  seqf1olem1  11367  facndiv  11584  cnpart  12050  rlimuni  12349  rlimcld2  12377  isercoll  12466  incexclem  12621  isumltss  12633  alzdvds  12904  fzm1ndvds  12906  fzo0dvdseq  12907  bitsfzolem  12951  smuval2  12999  smupvallem  13000  bezoutlem3  13045  rpdvds  13129  nonsq  13156  prmdiv  13179  odzdvds  13186  pcprendvds  13219  pcprendvds2  13220  pcpremul  13222  pcdvdsb  13247  pcadd2  13264  pockthlem  13278  prmreclem5  13293  prmreclem6  13294  1arith  13300  4sqlem11  13328  vdwlem11  13364  vdwlem12  13365  ramubcl  13391  mrissmrcd  13870  pltnlt  14430  acsfiindd  14608  odcl2  15206  gexnnod  15227  pgpssslw  15253  torsubg  15474  lt6abl  15509  ablfacrplem  15628  pgpfac1lem3  15640  irredrmul  15817  islbs3  16232  lbsextlem3  16237  lbsextlem4  16238  mvrf1  16494  perfopn  17254  pnfnei  17289  mnfnei  17290  haust1  17421  cmpcld  17470  ptbasfi  17618  fbncp  17876  isfild  17895  fbasfip  17905  filufint  17957  rnelfmlem  17989  fmfnfm  17995  fclscf  18062  ptcmplem3  18090  opnsubg  18142  bldisj  18433  iccntr  18857  icccmplem2  18859  reconnlem1  18862  reconnlem2  18863  evth  18989  lebnumlem3  18993  ovolicc2lem3  19420  volfiniun  19446  iundisj  19447  dvne0  19900  lhop2  19904  itgsubstlem  19937  coemullem  20173  plyexmo  20235  wilthlem2  20857  wilth  20859  mumul  20969  chtublem  21000  perfect1  21017  lgsdilem2  21120  lgsne0  21122  lgsqrlem2  21131  lgseisenlem1  21138  lgseisenlem2  21139  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  lgsquad2lem1  21147  2sqblem  21166  chebbnd1lem1  21168  pntpbnd2  21286  pntlem3  21308  ostth  21338  vdgr1a  21682  chirredlem1  23898  iundisjf  24034  iundisjfi  24157  logccne0  24401  lgamgulmlem1  24818  dedekind  25192  fundmpss  25395  dfon2lem4  25418  dfon2lem7  25421  sltval2  25616  sltasym  25632  broutsideof2  26061  outsidele  26071  onint1  26204  nn0prpwlem  26339  nn0prpw  26340  pellexlem6  26911  elpell14qr2  26939  pellfundglb  26962  jm2.19  27078  jm2.26lem3  27086  setindtr  27109  harinf  27119  f1lindf  27283  dgraa0p  27345  lpssat  29885  exatleN  30275  3noncolr2  30320  4noncolr3  30324  3dimlem3  30332  3dimlem3OLDN  30333  3dimlem4a  30334  3dimlem4  30335  3dimlem4OLDN  30336  3atlem4  30357  3atlem5  30358  3atlem6  30359  llnnleat  30384  lplnnle2at  30412  lvolnle3at  30453  4atlem0a  30464  4atlem0ae  30465  dalem21  30565  dalem54  30597  cdlemblem  30664  lhpmcvr4N  30897  4atexlemnclw  30941  cdlemd3  31071  cdleme3g  31105  cdleme3h  31106  cdleme7aa  31113  cdleme7d  31117  cdleme7ga  31119  cdleme11c  31132  cdleme15b  31146  cdleme20zN  31172  cdleme20y  31173  cdleme21b  31197  cdleme21c  31198  cdleme21ct  31200  cdleme22b  31212  cdleme32b  31313  cdleme35fnpq  31320  cdleme35f  31325  cdleme36a  31331  cdleme42c  31343  cdleme48bw  31373  cdlemf1  31432  cdlemg2fv2  31471  cdlemg7fvbwN  31478  cdlemg4  31488  cdlemg6c  31491  cdlemg27a  31563  cdlemg27b  31567  cdlemk3  31704  dia2dimlem1  31936  dihord6apre  32128  dihord6b  32132  dihord5apre  32134  dihglbcpreN  32172  dihmeetlem6  32181  dochnel2  32264  dochexmidlem7  32338  lspindp5  32642  mapdh8b  32652  hdmapip0  32790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator