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  eqneltrrd  2527  neleqtrd  2528  eueq3  3123  efrirr  4688  efrn2lp  4689  epne3  6381  ordtypelem9  7728  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1  7885  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1OLD  7908  cnfcom3lem  7924  cnfcom3lemOLD  7932  cflim2  8420  fin23lem30  8499  isf32lem5  8514  axdc3lem4  8610  axpownd  8755  pwfseqlem3  8814  grur1  8974  genpnnp  9161  xrlttri  11103  infmxrlb  11283  expneg  11856  bcval5  12077  hashge2el2dif  12167  seqcoll  12199  seqcoll2  12200  lswccatn0lsw  12270  fsumss  13185  rpdvds  13792  pcmpt  13936  prmreclem2  13960  prmreclem5  13963  prmlem0  14115  sylow1lem3  16078  sylow2blem3  16100  efgredlema  16216  gsum2d2lem  16438  lindsind2  18089  1stccnp  18907  kqdisj  19146  alexsubALTlem4  19463  xrhmeo  20359  minveclem3b  20756  ovolgelb  20804  volsup  20878  volsup2  20926  itg1val2  21003  itg2seq  21061  itg2cn  21082  limcnlp  21194  itgsubstlem  21361  ply1termlem  21555  radcnvlt1  21767  fsumharmonic  22289  ftalem3  22296  chpub  22443  lgsqr  22569  lgseisenlem1  22572  lgsquadlem3  22579  2sqlem8a  22594  2sqlem8  22595  2sqblem  22600  axcontlem2  23033  usgraedgrnv  23118  minvecolem5  24104  divnumden2  25909  oddpwdc  26584  eulerpartlemsv2  26588  eulerpartlemv  26594  eulerpartlemgh  26608  signslema  26810  erdszelem7  26932  erdszelem8  26933  fprodss  27307  wfrlem10  27579  wsuclem  27608  wsuclb  27611  ftc1anclem5  28312  cntotbnd  28536  irrapxlem1  29005  elpell14qr2  29045  elpell1qr2  29055  wepwsolem  29236  fnwe2lem2  29246  stoweidlem34  29672  stirlinglem5  29716  lshpdisj  32202  lcv1  32256  atlatmstc  32534  hlatcon2  32666  4noncolr3  32667  3atlem6  32702  lplnnleat  32756  lplnexllnN  32778  lvolnleat  32797  4atlem11  32823  dalem1  32873  dalemswapyzps  32904  dalemrotps  32905  2llnma1  33001  dalawlem15  33099  4atexlemcnd  33286  ltrnel  33353  cdleme15c  33490  cdleme0nex  33504  cdleme20y  33516  cdleme20m  33537  cdleme43bN  33704  cdleme43dN  33706  cdlemeg46nlpq  33731  cdlemg12  33864  dihmeetcN  34517  dihjatc1  34526  dihjatcclem1  34633  lclkrlem2a  34722  lcfrlem20  34777  mapdh6aN  34950  mapdh8ab  34992  hdmap1l6a  35025
  Copyright terms: Public domain W3C validator