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

Theorem mtod 177
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 25 . 2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
41, 3pm2.65d 175 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mtoi  178  mtbid  300  mtbird  301  mtand  652  mtord  653  po2nr  4641  po3nr  4642  ordn2lp  4726  onssneli  4815  tfi  6453  nnlim  6478  smoord  6812  tz7.48-3  6885  oalimcl  6987  omlimcl  7005  oneo  7008  omopth2  7011  nnneo  7078  mapdom2  7470  php3  7485  onomeneq  7488  sucdom2  7495  isfinite2  7558  domunfican  7572  ordtypelem7  7726  unxpwdom2  7791  cantnfp1lem2  7875  oemapvali  7880  cantnflem1  7885  cantnflem2  7886  cantnfp1lem2OLD  7901  cantnflem1OLD  7908  rankpwi  8018  tskwe  8108  alephordi  8232  alephdom  8239  cardaleph  8247  cflim2  8420  isfin4-3  8472  fin23lem26  8482  fin1a2lem13  8569  axcclem  8614  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwe2  8798  pwxpndom2  8820  pwxpndom  8821  pwcdandom  8822  gchaleph  8826  r1wunlim  8892  inatsk  8933  tskuni  8938  gruina  8973  prlem934  9190  dedekind  9521  qextltlem  11160  ixxub  11309  ixxlb  11310  seqf1olem1  11829  facndiv  12048  cnpart  12713  rlimuni  13012  rlimcld2  13040  isercoll  13129  incexclem  13282  isumltss  13294  alzdvds  13566  fzm1ndvds  13568  fzo0dvdseq  13569  bitsfzolem  13613  smuval2  13661  smupvallem  13662  bezoutlem3  13707  rpdvds  13793  nonsq  13820  prmdiv  13843  odzdvds  13850  pcprendvds  13890  pcprendvds2  13891  pcpremul  13893  pcdvdsb  13918  pcadd2  13935  pockthlem  13949  prmreclem5  13964  prmreclem6  13965  1arith  13971  4sqlem11  13999  vdwlem11  14035  vdwlem12  14036  ramubcl  14062  mrissmrcd  14561  pltnlt  15121  acsfiindd  15330  odcl2  16046  gexnnod  16067  pgpssslw  16093  torsubg  16316  lt6abl  16351  ablfacrplem  16540  pgpfac1lem3  16552  irredrmul  16733  islbs3  17158  lbsextlem3  17163  lbsextlem4  17164  mvrf1  17432  f1lindf  18093  perfopn  18631  pnfnei  18666  mnfnei  18667  haust1  18798  cmpcld  18847  ptbasfi  18996  fbncp  19254  isfild  19273  fbasfip  19283  filufint  19335  rnelfmlem  19367  fmfnfm  19373  fclscf  19440  ptcmplem3  19468  opnsubg  19520  bldisj  19815  iccntr  20240  icccmplem2  20242  reconnlem1  20245  reconnlem2  20246  evth  20373  lebnumlem3  20377  ovolicc2lem3  20844  volfiniun  20870  iundisj  20871  dvne0  21325  lhop2  21329  itgsubstlem  21362  coemullem  21602  plyexmo  21664  wilthlem2  22292  wilth  22294  mumul  22404  chtublem  22435  perfect1  22452  lgsdilem2  22555  lgsne0  22557  lgsqrlem2  22566  lgseisenlem1  22573  lgseisenlem2  22574  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  lgsquad2lem1  22582  2sqblem  22601  chebbnd1lem1  22603  pntpbnd2  22721  pntlem3  22743  ostth  22773  vdgr1a  23399  chirredlem1  25617  iundisjf  25755  iundisjfi  25903  logccne0  26309  lgamgulmlem1  26863  fundmpss  27424  dfon2lem4  27446  dfon2lem7  27449  sltval2  27644  sltasym  27660  broutsideof2  28000  outsidele  28010  onint1  28143  fin2so  28260  nn0prpwlem  28361  nn0prpw  28362  pellexlem6  29020  elpell14qr2  29048  pellfundglb  29071  jm2.19  29187  jm2.26lem3  29195  setindtr  29218  harinf  29228  dgraa0p  29351  rng1nfld  30736  lpssat  32231  exatleN  32621  3noncolr2  32666  4noncolr3  32670  3dimlem3  32678  3dimlem3OLDN  32679  3dimlem4a  32680  3dimlem4  32681  3dimlem4OLDN  32682  3atlem4  32703  3atlem5  32704  3atlem6  32705  llnnleat  32730  lplnnle2at  32758  lvolnle3at  32799  4atlem0a  32810  4atlem0ae  32811  dalem21  32911  dalem54  32943  cdlemblem  33010  lhpmcvr4N  33243  4atexlemnclw  33287  cdlemd3  33417  cdleme3g  33451  cdleme3h  33452  cdleme7aa  33459  cdleme7d  33463  cdleme7ga  33465  cdleme11c  33478  cdleme15b  33492  cdleme20zN  33518  cdleme20y  33519  cdleme21b  33543  cdleme21c  33544  cdleme21ct  33546  cdleme22b  33558  cdleme32b  33659  cdleme35fnpq  33666  cdleme35f  33671  cdleme36a  33677  cdleme42c  33689  cdleme48bw  33719  cdlemf1  33778  cdlemg2fv2  33817  cdlemg7fvbwN  33824  cdlemg4  33834  cdlemg6c  33837  cdlemg27a  33909  cdlemg27b  33913  cdlemk3  34050  dia2dimlem1  34282  dihord6apre  34474  dihord6b  34478  dihord5apre  34480  dihglbcpreN  34518  dihmeetlem6  34527  dochnel2  34610  dochexmidlem7  34684  lspindp5  34988  mapdh8b  34998  hdmapip0  35136
  Copyright terms: Public domain W3C validator