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

Theorem mtbid 301
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 226 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 180 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  sylnib  305  eqneltrrdOLD  2533  neleqtrd  2534  eueq3  3246  efrirr  4831  efrn2lp  4832  epne3  6618  wfrlem10  7050  ordtypelem9  8044  cantnfp1lem3  8187  cantnflem1b  8193  cantnflem1  8196  cnfcom3lem  8210  cflim2  8694  fin23lem30  8773  isf32lem5  8788  axdc3lem4  8884  axpownd  9027  pwfseqlem3  9086  grur1  9246  genpnnp  9431  xrlttri  11439  infmxrlbOLD  11625  expneg  12280  bcval5  12503  seqcoll  12625  seqcoll2  12626  hashge2el2dif  12634  fsumss  13779  fprodss  13990  rpdvds  14664  pcmpt  14825  prmreclem2  14849  prmreclem5  14852  prmlem0  15065  sylow1lem3  17240  sylow2blem3  17262  efgredlema  17378  gsum2d2lem  17593  lindsind2  19364  1stccnp  20464  kqdisj  20734  alexsubALTlem4  21052  xrhmeo  21961  minveclem3b  22357  minveclem3bOLD  22369  ovolgelb  22420  volsup  22496  volsup2  22550  itg1val2  22629  itg2seq  22687  itg2cn  22708  limcnlp  22820  itgsubstlem  22987  ply1termlem  23144  radcnvlt1  23360  fsumharmonic  23924  ftalem3  23986  chpub  24135  lgsqr  24261  lgseisenlem1  24264  lgsquadlem3  24271  2sqlem8a  24286  2sqlem8  24287  2sqblem  24292  tgdim01  24538  lnoppnhpg  24793  acopyeu  24862  axcontlem2  24982  usgraedgrnv  25091  minvecolem5  26509  minvecolem5OLD  26519  divnumden2  28376  esum2d  28910  oddpwdc  29183  eulerpartlemsv2  29187  eulerpartlemv  29193  eulerpartlemgh  29207  signslema  29447  erdszelem7  29916  erdszelem8  29917  wsuclem  30503  wsuclb  30506  ftc1anclem5  31935  cntotbnd  32042  lshpdisj  32472  lcv1  32526  atlatmstc  32804  hlatcon2  32936  4noncolr3  32937  3atlem6  32972  lplnnleat  33026  lplnexllnN  33048  lvolnleat  33067  4atlem11  33093  dalem1  33143  dalemswapyzps  33174  dalemrotps  33175  2llnma1  33271  dalawlem15  33369  4atexlemcnd  33556  ltrnel  33623  cdleme15c  33761  cdleme0nex  33775  cdleme20yOLD  33788  cdleme20m  33809  cdleme43bN  33976  cdleme43dN  33978  cdlemeg46nlpq  34003  cdlemg12  34136  dihmeetcN  34789  dihjatc1  34798  dihjatcclem1  34905  lclkrlem2a  34994  lcfrlem20  35049  mapdh6aN  35222  mapdh8ab  35264  hdmap1l6a  35297  irrapxlem1  35586  elpell14qr2  35628  elpell1qr2  35638  wepwsolem  35820  fnwe2lem2  35829  oddfl  37329  dstregt0  37333  xrlttri5d  37335  divlt0gt0d  37338  supxrgere  37398  supxrgelem  37402  supxrge  37403  suplesup  37404  nepnfltpnf  37407  nemnftgtmnft  37409  infrpge  37416  iccdifprioo  37448  stoweidlem34  37715  stirlinglem5  37760  dirker2re  37774  dirkerdenne0  37775  dirkertrigeq  37783  dirkercncflem2  37786  dirkercncflem4  37788  fourierdlem54  37844  elaa2lem  37917  elaa2lemOLD  37918  etransclem9  37928  sge0cl  38011  sge0repnf  38016  sge0split  38039  0nodd  39082  2nodd  39084  1neven  39204
  Copyright terms: Public domain W3C validator