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

Theorem mtbid 300
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)
Hypotheses
Ref Expression
mtbid.min  |-  ( ph  ->  -.  ps )
mtbid.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbid  |-  ( ph  ->  -.  ch )

Proof of Theorem mtbid
StepHypRef Expression
1 mtbid.min . 2  |-  ( ph  ->  -.  ps )
2 mtbid.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimprd 223 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 177 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  sylnib  304  eqneltrrd  2536  neleqtrd  2537  eueq3  3133  efrirr  4700  efrn2lp  4701  epne3  6391  ordtypelem9  7739  cantnfp1lem3  7887  cantnflem1b  7893  cantnflem1  7896  cantnfp1lem3OLD  7913  cantnflem1bOLD  7916  cantnflem1OLD  7919  cnfcom3lem  7935  cnfcom3lemOLD  7943  cflim2  8431  fin23lem30  8510  isf32lem5  8525  axdc3lem4  8621  axpownd  8766  pwfseqlem3  8826  grur1  8986  genpnnp  9173  xrlttri  11115  infmxrlb  11295  expneg  11872  bcval5  12093  hashge2el2dif  12183  seqcoll  12215  seqcoll2  12216  lswccatn0lsw  12286  fsumss  13201  rpdvds  13809  pcmpt  13953  prmreclem2  13977  prmreclem5  13980  prmlem0  14132  sylow1lem3  16098  sylow2blem3  16120  efgredlema  16236  gsum2d2lem  16464  lindsind2  18247  1stccnp  19065  kqdisj  19304  alexsubALTlem4  19621  xrhmeo  20517  minveclem3b  20914  ovolgelb  20962  volsup  21036  volsup2  21084  itg1val2  21161  itg2seq  21219  itg2cn  21240  limcnlp  21352  itgsubstlem  21519  ply1termlem  21670  radcnvlt1  21882  fsumharmonic  22404  ftalem3  22411  chpub  22558  lgsqr  22684  lgseisenlem1  22687  lgsquadlem3  22694  2sqlem8a  22709  2sqlem8  22710  2sqblem  22715  axcontlem2  23210  usgraedgrnv  23295  minvecolem5  24281  divnumden2  26086  oddpwdc  26736  eulerpartlemsv2  26740  eulerpartlemv  26746  eulerpartlemgh  26760  signslema  26962  erdszelem7  27084  erdszelem8  27085  fprodss  27460  wfrlem10  27732  wsuclem  27761  wsuclb  27764  ftc1anclem5  28469  cntotbnd  28693  irrapxlem1  29161  elpell14qr2  29201  elpell1qr2  29211  wepwsolem  29392  fnwe2lem2  29402  stoweidlem34  29827  stirlinglem5  29871  lshpdisj  32630  lcv1  32684  atlatmstc  32962  hlatcon2  33094  4noncolr3  33095  3atlem6  33130  lplnnleat  33184  lplnexllnN  33206  lvolnleat  33225  4atlem11  33251  dalem1  33301  dalemswapyzps  33332  dalemrotps  33333  2llnma1  33429  dalawlem15  33527  4atexlemcnd  33714  ltrnel  33781  cdleme15c  33918  cdleme0nex  33932  cdleme20y  33944  cdleme20m  33965  cdleme43bN  34132  cdleme43dN  34134  cdlemeg46nlpq  34159  cdlemg12  34292  dihmeetcN  34945  dihjatc1  34954  dihjatcclem1  35061  lclkrlem2a  35150  lcfrlem20  35205  mapdh6aN  35378  mapdh8ab  35420  hdmap1l6a  35453
  Copyright terms: Public domain W3C validator