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  2482  neleqtrd  2483  eueq3  3053  efrirr  4505  efrn2lp  4506  epne3  4702  ordtypelem9  7429  cantnfp1lem3  7570  cantnflem1b  7576  cantnflem1  7579  cnfcom3lem  7594  cflim2  8077  fin23lem30  8156  isf32lem5  8171  axdc3lem4  8267  axpownd  8410  pwfseqlem3  8469  grur1  8629  genpnnp  8816  xrlttri  10665  infmxrlb  10845  expneg  11317  bcval5  11537  seqcoll  11640  seqcoll2  11641  fsumss  12447  rpdvds  13052  pcmpt  13189  prmreclem2  13213  prmreclem5  13216  prmlem0  13356  sylow1lem3  15162  sylow2blem3  15184  efgredlema  15300  gsum2d2lem  15475  1stccnp  17447  kqdisj  17686  alexsubALTlem4  18003  xrhmeo  18843  minveclem3b  19197  ovolgelb  19244  volsup  19318  volsup2  19365  itg1val2  19444  itg2seq  19502  itg2cn  19523  limcnlp  19633  itgsubstlem  19800  ply1termlem  19990  radcnvlt1  20202  fsumharmonic  20718  ftalem3  20725  chpub  20872  lgsqr  20998  lgseisenlem1  21001  lgsquadlem3  21008  2sqlem8a  21023  2sqlem8  21024  2sqblem  21029  usgraedgrnv  21265  minvecolem5  22232  divnumden2  24000  erdszelem7  24663  erdszelem8  24664  fprodss  25054  wfrlem10  25290  axcontlem2  25619  cntotbnd  26197  irrapxlem1  26577  elpell14qr2  26617  elpell1qr2  26627  wepwsolem  26808  fnwe2lem2  26818  lindsind2  26959  stoweidlem34  27452  stirlinglem5  27496  lshpdisj  29103  lcv1  29157  atlatmstc  29435  hlatcon2  29567  4noncolr3  29568  3atlem6  29603  lplnnleat  29657  lplnexllnN  29679  lvolnleat  29698  4atlem11  29724  dalem1  29774  dalemswapyzps  29805  dalemrotps  29806  2llnma1  29902  dalawlem15  30000  4atexlemcnd  30187  ltrnel  30254  cdleme15c  30391  cdleme0nex  30405  cdleme20y  30417  cdleme20m  30438  cdleme43bN  30605  cdleme43dN  30607  cdlemeg46nlpq  30632  cdlemg12  30765  dihmeetcN  31418  dihjatc1  31427  dihjatcclem1  31534  lclkrlem2a  31623  lcfrlem20  31678  mapdh6aN  31851  mapdh8ab  31893  hdmap1l6a  31926
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