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

Theorem mtbid 298
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  302  eqneltrrdOLD  2565  neleqtrd  2566  eueq3  3271  efrirr  4849  efrn2lp  4850  epne3  6589  ordtypelem9  7943  cantnfp1lem3  8090  cantnflem1b  8096  cantnflem1  8099  cantnfp1lem3OLD  8116  cantnflem1bOLD  8119  cantnflem1OLD  8122  cnfcom3lem  8138  cnfcom3lemOLD  8146  cflim2  8634  fin23lem30  8713  isf32lem5  8728  axdc3lem4  8824  axpownd  8967  pwfseqlem3  9027  grur1  9187  genpnnp  9372  xrlttri  11348  infmxrlb  11528  expneg  12156  bcval5  12378  seqcoll  12496  seqcoll2  12497  hashge2el2dif  12505  fsumss  13629  fprodss  13837  rpdvds  14349  pcmpt  14495  prmreclem2  14519  prmreclem5  14522  prmlem0  14675  sylow1lem3  16819  sylow2blem3  16841  efgredlema  16957  gsum2d2lem  17197  lindsind2  19021  1stccnp  20129  kqdisj  20399  alexsubALTlem4  20716  xrhmeo  21612  minveclem3b  22009  ovolgelb  22057  volsup  22132  volsup2  22180  itg1val2  22257  itg2seq  22315  itg2cn  22336  limcnlp  22448  itgsubstlem  22615  ply1termlem  22766  radcnvlt1  22979  fsumharmonic  23539  ftalem3  23546  chpub  23693  lgsqr  23819  lgseisenlem1  23822  lgsquadlem3  23829  2sqlem8a  23844  2sqlem8  23845  2sqblem  23850  tgdim01  24099  lnoppnhpg  24334  axcontlem2  24470  usgraedgrnv  24579  minvecolem5  25995  divnumden2  27843  esum2d  28322  oddpwdc  28557  eulerpartlemsv2  28561  eulerpartlemv  28567  eulerpartlemgh  28581  signslema  28783  erdszelem7  28905  erdszelem8  28906  wfrlem10  29592  wsuclem  29621  wsuclb  29624  ftc1anclem5  30334  cntotbnd  30532  irrapxlem1  30997  elpell14qr2  31037  elpell1qr2  31047  wepwsolem  31226  fnwe2lem2  31236  oddfl  31699  dstregt0  31703  xrlttri5d  31705  divlt0gt0d  31709  iccdifprioo  31795  stoweidlem34  32055  stirlinglem5  32099  dirker2re  32113  dirkerdenne0  32114  dirkertrigeq  32122  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem54  32182  elaa2lem  32255  etransclem9  32265  0nodd  32870  2nodd  32872  1neven  32992  lshpdisj  35109  lcv1  35163  atlatmstc  35441  hlatcon2  35573  4noncolr3  35574  3atlem6  35609  lplnnleat  35663  lplnexllnN  35685  lvolnleat  35704  4atlem11  35730  dalem1  35780  dalemswapyzps  35811  dalemrotps  35812  2llnma1  35908  dalawlem15  36006  4atexlemcnd  36193  ltrnel  36260  cdleme15c  36398  cdleme0nex  36412  cdleme20yOLD  36425  cdleme20m  36446  cdleme43bN  36613  cdleme43dN  36615  cdlemeg46nlpq  36640  cdlemg12  36773  dihmeetcN  37426  dihjatc1  37435  dihjatcclem1  37542  lclkrlem2a  37631  lcfrlem20  37686  mapdh6aN  37859  mapdh8ab  37901  hdmap1l6a  37934
  Copyright terms: Public domain W3C validator