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

Theorem mtod 170
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 23 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
41, 3pm2.65d 168 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mtoi  171  mtbid  292  mtbird  293  mtand  641  mtord  642  po2nr  4508  po3nr  4509  ordn2lp  4593  onssneli  4683  tfi  4825  nnlim  4850  smoord  6619  tz7.48-3  6693  oalimcl  6795  omlimcl  6813  oneo  6816  omopth2  6819  nnneo  6886  mapdom2  7270  php3  7285  onomeneq  7288  sucdom2  7295  isfinite2  7357  domunfican  7371  ordtypelem7  7485  unxpwdom2  7548  cantnfp1lem2  7627  oemapvali  7632  cantnflem1  7637  cantnflem2  7638  rankpwi  7741  tskwe  7829  alephordi  7947  alephdom  7954  cardaleph  7962  cflim2  8135  isfin4-3  8187  fin23lem26  8197  fin1a2lem13  8284  axcclem  8329  fpwwe2lem12  8508  fpwwe2lem13  8509  fpwwe2  8510  pwxpndom2  8532  pwxpndom  8533  pwcdandom  8534  gchaleph  8542  r1wunlim  8604  inatsk  8645  tskuni  8650  gruina  8685  prlem934  8902  qextltlem  10780  ixxub  10929  ixxlb  10930  seqf1olem1  11354  facndiv  11571  cnpart  12037  rlimuni  12336  rlimcld2  12364  isercoll  12453  incexclem  12608  isumltss  12620  alzdvds  12891  fzm1ndvds  12893  fzo0dvdseq  12894  bitsfzolem  12938  smuval2  12986  smupvallem  12987  bezoutlem3  13032  rpdvds  13116  nonsq  13143  prmdiv  13166  odzdvds  13173  pcprendvds  13206  pcprendvds2  13207  pcpremul  13209  pcdvdsb  13234  pcadd2  13251  pockthlem  13265  prmreclem5  13280  prmreclem6  13281  1arith  13287  4sqlem11  13315  vdwlem11  13351  vdwlem12  13352  ramubcl  13378  mrissmrcd  13857  pltnlt  14417  acsfiindd  14595  odcl2  15193  gexnnod  15214  pgpssslw  15240  torsubg  15461  lt6abl  15496  ablfacrplem  15615  pgpfac1lem3  15627  irredrmul  15804  islbs3  16219  lbsextlem3  16224  lbsextlem4  16225  mvrf1  16481  perfopn  17241  pnfnei  17276  mnfnei  17277  haust1  17408  cmpcld  17457  ptbasfi  17605  fbncp  17863  isfild  17882  fbasfip  17892  filufint  17944  rnelfmlem  17976  fmfnfm  17982  fclscf  18049  ptcmplem3  18077  opnsubg  18129  bldisj  18420  iccntr  18844  icccmplem2  18846  reconnlem1  18849  reconnlem2  18850  evth  18976  lebnumlem3  18980  ovolicc2lem3  19407  volfiniun  19433  iundisj  19434  dvne0  19887  lhop2  19891  itgsubstlem  19924  coemullem  20160  plyexmo  20222  wilthlem2  20844  wilth  20846  mumul  20956  chtublem  20987  perfect1  21004  lgsdilem2  21107  lgsne0  21109  lgsqrlem2  21118  lgseisenlem1  21125  lgseisenlem2  21126  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  lgsquad2lem1  21134  2sqblem  21153  chebbnd1lem1  21155  pntpbnd2  21273  pntlem3  21295  ostth  21325  vdgr1a  21669  chirredlem1  23885  iundisjf  24021  iundisjfi  24144  logccne0  24388  lgamgulmlem1  24805  dedekind  25179  fundmpss  25382  dfon2lem4  25405  dfon2lem7  25408  sltval2  25603  sltasym  25619  broutsideof2  26048  outsidele  26058  onint1  26191  nn0prpwlem  26316  nn0prpw  26317  pellexlem6  26888  elpell14qr2  26916  pellfundglb  26939  jm2.19  27055  jm2.26lem3  27063  setindtr  27086  harinf  27096  f1lindf  27260  dgraa0p  27322  lpssat  29748  exatleN  30138  3noncolr2  30183  4noncolr3  30187  3dimlem3  30195  3dimlem3OLDN  30196  3dimlem4a  30197  3dimlem4  30198  3dimlem4OLDN  30199  3atlem4  30220  3atlem5  30221  3atlem6  30222  llnnleat  30247  lplnnle2at  30275  lvolnle3at  30316  4atlem0a  30327  4atlem0ae  30328  dalem21  30428  dalem54  30460  cdlemblem  30527  lhpmcvr4N  30760  4atexlemnclw  30804  cdlemd3  30934  cdleme3g  30968  cdleme3h  30969  cdleme7aa  30976  cdleme7d  30980  cdleme7ga  30982  cdleme11c  30995  cdleme15b  31009  cdleme20zN  31035  cdleme20y  31036  cdleme21b  31060  cdleme21c  31061  cdleme21ct  31063  cdleme22b  31075  cdleme32b  31176  cdleme35fnpq  31183  cdleme35f  31188  cdleme36a  31194  cdleme42c  31206  cdleme48bw  31236  cdlemf1  31295  cdlemg2fv2  31334  cdlemg7fvbwN  31341  cdlemg4  31351  cdlemg6c  31354  cdlemg27a  31426  cdlemg27b  31430  cdlemk3  31567  dia2dimlem1  31799  dihord6apre  31991  dihord6b  31995  dihord5apre  31997  dihglbcpreN  32035  dihmeetlem6  32044  dochnel2  32127  dochexmidlem7  32201  lspindp5  32505  mapdh8b  32515  hdmapip0  32653
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator