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

Theorem mtbid 291
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 214 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 168 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  sylnib  295  eqneltrrd  2377  neleqtrd  2378  eueq3  2940  efrirr  4374  efrn2lp  4375  epne3  4572  smoord  6382  ordtypelem9  7241  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1  7391  cnfcom3lem  7406  cflim2  7889  fin23lem30  7968  isf32lem5  7983  axdc3lem4  8079  axpownd  8223  pwfseqlem3  8282  r1tskina  8404  grur1  8442  genpnnp  8629  xrlttri  10473  infmxrlb  10652  expneg  11111  bcval5  11330  seqcoll  11401  seqcoll2  11402  fsumss  12198  bitsf1  12637  rpdvds  12803  pcmpt  12940  prmreclem2  12964  prmreclem5  12967  prmlem0  13107  sylow1lem3  14911  sylow2blem3  14933  efgredlema  15049  gsum2d2lem  15224  lssvancl2  15703  lbsind2  15834  1stccnp  17188  kqdisj  17423  alexsubALTlem4  17744  xrhmeo  18444  minveclem3b  18792  ovolgelb  18839  volsup  18913  volsup2  18960  itg1val2  19039  itg2seq  19097  itg2cn  19118  limcnlp  19228  itgsubstlem  19395  ply1termlem  19585  radcnvlt1  19794  fsumharmonic  20305  ftalem3  20312  chpub  20459  lgsqr  20585  lgseisenlem1  20588  lgsquadlem3  20595  2sqlem8a  20610  2sqlem8  20611  2sqblem  20616  minvecolem5  21460  erdszelem7  23728  erdszelem8  23729  wfrlem10  24265  axcontlem2  24593  cntotbnd  26520  irrapxlem1  26907  elpell14qr2  26947  elpell1qr2  26957  wepwsolem  27138  fnwe2lem2  27148  lindfind2  27288  lindsind2  27289  stoweidlem26  27775  stoweidlem34  27783  stirlinglem5  27827  usgraedgrnv  28123  lshpdisj  29177  lcv1  29231  atlatmstc  29509  hlatcon2  29641  4noncolr3  29642  2atjlej  29668  3atlem6  29677  lplnnleat  29731  lplnexllnN  29753  lvolnleat  29772  2atnelvolN  29776  4atlem11  29798  dalem1  29848  dalemswapyzps  29879  dalemrotps  29880  2llnma1  29976  dalawlem15  30074  4atexlemcnd  30261  ltrnel  30328  cdleme15c  30465  cdleme0nex  30479  cdleme20y  30491  cdleme20m  30512  cdleme43bN  30679  cdleme43dN  30681  cdlemeg46nlpq  30706  cdlemg12  30839  dihmeetcN  31492  dihjatc1  31501  dochnel  31583  dihjatcclem1  31608  lclkrlem2a  31697  lcfrlem20  31752  mapdh6aN  31925  mapdh8ab  31967  hdmap1l6a  32000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator