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

Theorem mtbid 292
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 215 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3mtod 170 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  sylnib  296  eqneltrrd  2529  neleqtrd  2530  eueq3  3101  efrirr  4555  efrn2lp  4556  epne3  4753  ordtypelem9  7487  cantnfp1lem3  7628  cantnflem1b  7634  cantnflem1  7637  cnfcom3lem  7652  cflim2  8135  fin23lem30  8214  isf32lem5  8229  axdc3lem4  8325  axpownd  8468  pwfseqlem3  8527  grur1  8687  genpnnp  8874  xrlttri  10724  infmxrlb  10904  expneg  11381  bcval5  11601  seqcoll  11704  seqcoll2  11705  fsumss  12511  rpdvds  13116  pcmpt  13253  prmreclem2  13277  prmreclem5  13280  prmlem0  13420  sylow1lem3  15226  sylow2blem3  15248  efgredlema  15364  gsum2d2lem  15539  1stccnp  17517  kqdisj  17756  alexsubALTlem4  18073  xrhmeo  18963  minveclem3b  19321  ovolgelb  19368  volsup  19442  volsup2  19489  itg1val2  19568  itg2seq  19626  itg2cn  19647  limcnlp  19757  itgsubstlem  19924  ply1termlem  20114  radcnvlt1  20326  fsumharmonic  20842  ftalem3  20849  chpub  20996  lgsqr  21122  lgseisenlem1  21125  lgsquadlem3  21132  2sqlem8a  21147  2sqlem8  21148  2sqblem  21153  usgraedgrnv  21389  minvecolem5  22375  divnumden2  24153  erdszelem7  24875  erdszelem8  24876  fprodss  25266  wfrlem10  25539  wsuclem  25568  wsuclb  25571  axcontlem2  25896  ftc1anclem5  26274  cntotbnd  26496  irrapxlem1  26876  elpell14qr2  26916  elpell1qr2  26926  wepwsolem  27107  fnwe2lem2  27117  lindsind2  27257  stoweidlem34  27750  stirlinglem5  27794  cshwidxn  28213  lshpdisj  29722  lcv1  29776  atlatmstc  30054  hlatcon2  30186  4noncolr3  30187  3atlem6  30222  lplnnleat  30276  lplnexllnN  30298  lvolnleat  30317  4atlem11  30343  dalem1  30393  dalemswapyzps  30424  dalemrotps  30425  2llnma1  30521  dalawlem15  30619  4atexlemcnd  30806  ltrnel  30873  cdleme15c  31010  cdleme0nex  31024  cdleme20y  31036  cdleme20m  31057  cdleme43bN  31224  cdleme43dN  31226  cdlemeg46nlpq  31251  cdlemg12  31384  dihmeetcN  32037  dihjatc1  32046  dihjatcclem1  32153  lclkrlem2a  32242  lcfrlem20  32297  mapdh6aN  32470  mapdh8ab  32512  hdmap1l6a  32545
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 178
  Copyright terms: Public domain W3C validator