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

Theorem mtbid 300
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  304  eqneltrrdOLD  2578  neleqtrd  2579  eueq3  3278  efrirr  4860  efrn2lp  4861  epne3  6600  ordtypelem9  7951  cantnfp1lem3  8099  cantnflem1b  8105  cantnflem1  8108  cantnfp1lem3OLD  8125  cantnflem1bOLD  8128  cantnflem1OLD  8131  cnfcom3lem  8147  cnfcom3lemOLD  8155  cflim2  8643  fin23lem30  8722  isf32lem5  8737  axdc3lem4  8833  axpownd  8978  pwfseqlem3  9038  grur1  9198  genpnnp  9383  xrlttri  11345  infmxrlb  11525  expneg  12142  bcval5  12364  seqcoll  12478  seqcoll2  12479  hashge2el2dif  12487  lswccatn0lsw  12571  fsumss  13510  rpdvds  14124  pcmpt  14270  prmreclem2  14294  prmreclem5  14297  prmlem0  14449  sylow1lem3  16426  sylow2blem3  16448  efgredlema  16564  gsum2d2lem  16804  lindsind2  18649  1stccnp  19757  kqdisj  19996  alexsubALTlem4  20313  xrhmeo  21209  minveclem3b  21606  ovolgelb  21654  volsup  21729  volsup2  21777  itg1val2  21854  itg2seq  21912  itg2cn  21933  limcnlp  22045  itgsubstlem  22212  ply1termlem  22363  radcnvlt1  22575  fsumharmonic  23097  ftalem3  23104  chpub  23251  lgsqr  23377  lgseisenlem1  23380  lgsquadlem3  23387  2sqlem8a  23402  2sqlem8  23403  2sqblem  23408  axcontlem2  23972  usgraedgrnv  24081  minvecolem5  25501  divnumden2  27304  oddpwdc  27961  eulerpartlemsv2  27965  eulerpartlemv  27971  eulerpartlemgh  27985  signslema  28187  erdszelem7  28309  erdszelem8  28310  fprodss  28685  wfrlem10  28957  wsuclem  28986  wsuclb  28989  ftc1anclem5  29699  cntotbnd  29923  irrapxlem1  30390  elpell14qr2  30430  elpell1qr2  30440  wepwsolem  30619  fnwe2lem2  30629  oddfl  31064  dstregt0  31068  xrlttri5d  31070  divlt0gt0d  31074  znnn0nn  31094  iccdifprioo  31148  stoweidlem34  31362  stirlinglem5  31406  dirker2re  31420  dirkerdenne0  31421  dirkerval2  31422  dirkertrigeq  31429  dirkercncflem2  31432  dirkercncflem4  31434  fourierdlem54  31489  lshpdisj  33802  lcv1  33856  atlatmstc  34134  hlatcon2  34266  4noncolr3  34267  3atlem6  34302  lplnnleat  34356  lplnexllnN  34378  lvolnleat  34397  4atlem11  34423  dalem1  34473  dalemswapyzps  34504  dalemrotps  34505  2llnma1  34601  dalawlem15  34699  4atexlemcnd  34886  ltrnel  34953  cdleme15c  35090  cdleme0nex  35104  cdleme20y  35116  cdleme20m  35137  cdleme43bN  35304  cdleme43dN  35306  cdlemeg46nlpq  35331  cdlemg12  35464  dihmeetcN  36117  dihjatc1  36126  dihjatcclem1  36233  lclkrlem2a  36322  lcfrlem20  36377  mapdh6aN  36550  mapdh8ab  36592  hdmap1l6a  36625
  Copyright terms: Public domain W3C validator