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  2390  neleqtrd  2391  eueq3  2953  efrirr  4390  efrn2lp  4391  epne3  4588  smoord  6398  ordtypelem9  7257  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  cnfcom3lem  7422  cflim2  7905  fin23lem30  7984  isf32lem5  7999  axdc3lem4  8095  axpownd  8239  pwfseqlem3  8298  r1tskina  8420  grur1  8458  genpnnp  8645  xrlttri  10489  infmxrlb  10668  expneg  11127  bcval5  11346  seqcoll  11417  seqcoll2  11418  fsumss  12214  bitsf1  12653  rpdvds  12819  pcmpt  12956  prmreclem2  12980  prmreclem5  12983  prmlem0  13123  sylow1lem3  14927  sylow2blem3  14949  efgredlema  15065  gsum2d2lem  15240  lssvancl2  15719  lbsind2  15850  1stccnp  17204  kqdisj  17439  alexsubALTlem4  17760  xrhmeo  18460  minveclem3b  18808  ovolgelb  18855  volsup  18929  volsup2  18976  itg1val2  19055  itg2seq  19113  itg2cn  19134  limcnlp  19244  itgsubstlem  19411  ply1termlem  19601  radcnvlt1  19810  fsumharmonic  20321  ftalem3  20328  chpub  20475  lgsqr  20601  lgseisenlem1  20604  lgsquadlem3  20611  2sqlem8a  20626  2sqlem8  20627  2sqblem  20632  minvecolem5  21476  erdszelem7  23743  erdszelem8  23744  wfrlem10  24336  axcontlem2  24665  cntotbnd  26623  irrapxlem1  27010  elpell14qr2  27050  elpell1qr2  27060  wepwsolem  27241  fnwe2lem2  27251  lindfind2  27391  lindsind2  27392  stoweidlem26  27878  stoweidlem34  27886  stirlinglem5  27930  usgraedgrnv  28257  lshpdisj  29799  lcv1  29853  atlatmstc  30131  hlatcon2  30263  4noncolr3  30264  2atjlej  30290  3atlem6  30299  lplnnleat  30353  lplnexllnN  30375  lvolnleat  30394  2atnelvolN  30398  4atlem11  30420  dalem1  30470  dalemswapyzps  30501  dalemrotps  30502  2llnma1  30598  dalawlem15  30696  4atexlemcnd  30883  ltrnel  30950  cdleme15c  31087  cdleme0nex  31101  cdleme20y  31113  cdleme20m  31134  cdleme43bN  31301  cdleme43dN  31303  cdlemeg46nlpq  31328  cdlemg12  31461  dihmeetcN  32114  dihjatc1  32123  dochnel  32205  dihjatcclem1  32230  lclkrlem2a  32319  lcfrlem20  32374  mapdh6aN  32547  mapdh8ab  32589  hdmap1l6a  32622
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