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

Theorem mtbid 293
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 216 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 171 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  sylnib  297  eqneltrrd  2532  neleqtrd  2533  eueq3  3111  efrirr  4566  efrn2lp  4567  epne3  4764  ordtypelem9  7498  cantnfp1lem3  7639  cantnflem1b  7645  cantnflem1  7648  cnfcom3lem  7663  cflim2  8148  fin23lem30  8227  isf32lem5  8242  axdc3lem4  8338  axpownd  8481  pwfseqlem3  8540  grur1  8700  genpnnp  8887  xrlttri  10737  infmxrlb  10917  expneg  11394  bcval5  11614  seqcoll  11717  seqcoll2  11718  fsumss  12524  rpdvds  13129  pcmpt  13266  prmreclem2  13290  prmreclem5  13293  prmlem0  13433  sylow1lem3  15239  sylow2blem3  15261  efgredlema  15377  gsum2d2lem  15552  1stccnp  17530  kqdisj  17769  alexsubALTlem4  18086  xrhmeo  18976  minveclem3b  19334  ovolgelb  19381  volsup  19455  volsup2  19502  itg1val2  19579  itg2seq  19637  itg2cn  19658  limcnlp  19770  itgsubstlem  19937  ply1termlem  20127  radcnvlt1  20339  fsumharmonic  20855  ftalem3  20862  chpub  21009  lgsqr  21135  lgseisenlem1  21138  lgsquadlem3  21145  2sqlem8a  21160  2sqlem8  21161  2sqblem  21166  usgraedgrnv  21402  minvecolem5  22388  divnumden2  24166  erdszelem7  24888  erdszelem8  24889  fprodss  25279  wfrlem10  25552  wsuclem  25581  wsuclb  25584  axcontlem2  25909  ftc1anclem5  26298  cntotbnd  26519  irrapxlem1  26899  elpell14qr2  26939  elpell1qr2  26949  wepwsolem  27130  fnwe2lem2  27140  lindsind2  27280  stoweidlem34  27773  stirlinglem5  27817  cshwidxn  28281  lshpdisj  29859  lcv1  29913  atlatmstc  30191  hlatcon2  30323  4noncolr3  30324  3atlem6  30359  lplnnleat  30413  lplnexllnN  30435  lvolnleat  30454  4atlem11  30480  dalem1  30530  dalemswapyzps  30561  dalemrotps  30562  2llnma1  30658  dalawlem15  30756  4atexlemcnd  30943  ltrnel  31010  cdleme15c  31147  cdleme0nex  31161  cdleme20y  31173  cdleme20m  31194  cdleme43bN  31361  cdleme43dN  31363  cdlemeg46nlpq  31388  cdlemg12  31521  dihmeetcN  32174  dihjatc1  32183  dihjatcclem1  32290  lclkrlem2a  32379  lcfrlem20  32434  mapdh6aN  32607  mapdh8ab  32649  hdmap1l6a  32682
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 179
  Copyright terms: Public domain W3C validator