MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbid 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  2498  neleqtrd  2499  eueq3  3069  efrirr  4523  efrn2lp  4524  epne3  4720  ordtypelem9  7451  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1  7601  cnfcom3lem  7616  cflim2  8099  fin23lem30  8178  isf32lem5  8193  axdc3lem4  8289  axpownd  8432  pwfseqlem3  8491  grur1  8651  genpnnp  8838  xrlttri  10688  infmxrlb  10868  expneg  11344  bcval5  11564  seqcoll  11667  seqcoll2  11668  fsumss  12474  rpdvds  13079  pcmpt  13216  prmreclem2  13240  prmreclem5  13243  prmlem0  13383  sylow1lem3  15189  sylow2blem3  15211  efgredlema  15327  gsum2d2lem  15502  1stccnp  17478  kqdisj  17717  alexsubALTlem4  18034  xrhmeo  18924  minveclem3b  19282  ovolgelb  19329  volsup  19403  volsup2  19450  itg1val2  19529  itg2seq  19587  itg2cn  19608  limcnlp  19718  itgsubstlem  19885  ply1termlem  20075  radcnvlt1  20287  fsumharmonic  20803  ftalem3  20810  chpub  20957  lgsqr  21083  lgseisenlem1  21086  lgsquadlem3  21093  2sqlem8a  21108  2sqlem8  21109  2sqblem  21114  usgraedgrnv  21350  minvecolem5  22336  divnumden2  24114  erdszelem7  24836  erdszelem8  24837  fprodss  25227  wfrlem10  25479  axcontlem2  25808  cntotbnd  26395  irrapxlem1  26775  elpell14qr2  26815  elpell1qr2  26825  wepwsolem  27006  fnwe2lem2  27016  lindsind2  27157  stoweidlem34  27650  stirlinglem5  27694  lshpdisj  29470  lcv1  29524  atlatmstc  29802  hlatcon2  29934  4noncolr3  29935  3atlem6  29970  lplnnleat  30024  lplnexllnN  30046  lvolnleat  30065  4atlem11  30091  dalem1  30141  dalemswapyzps  30172  dalemrotps  30173  2llnma1  30269  dalawlem15  30367  4atexlemcnd  30554  ltrnel  30621  cdleme15c  30758  cdleme0nex  30772  cdleme20y  30784  cdleme20m  30805  cdleme43bN  30972  cdleme43dN  30974  cdlemeg46nlpq  30999  cdlemg12  31132  dihmeetcN  31785  dihjatc1  31794  dihjatcclem1  31901  lclkrlem2a  31990  lcfrlem20  32045  mapdh6aN  32218  mapdh8ab  32260  hdmap1l6a  32293
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