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

Theorem mtbiri 303
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
Hypotheses
Ref Expression
mtbiri.min  |-  -.  ch
mtbiri.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbiri  |-  ( ph  ->  -.  ps )

Proof of Theorem mtbiri
StepHypRef Expression
1 mtbiri.min . 2  |-  -.  ch
2 mtbiri.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 207 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 178 1  |-  ( ph  ->  -.  ps )
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:  psstr  3608  n0i  3790  sbcel2  3831  sbcbr123  4498  axnul  4575  intex  4603  intnex  4604  iin0  4621  nfcvb  4677  opelopabsb  4757  0ellim  4940  0nelelxp  5028  onxpdisj  5083  elimasni  5364  ndmfvrcl  5891  canth  6242  brabv  6326  oprssdm  6440  ndmovrcl  6445  omelon2  6696  undefnel2  7006  tfr2b  7065  tz7.44-3  7074  omeulem1  7231  eceqoveq  7416  2dom  7588  omxpenlem  7618  domunsn  7667  disjen  7674  infensuc  7695  snnen2o  7706  elfi2  7874  sucprcregOLD  8026  en3lp  8033  preleq  8034  rankxpsuc  8300  sdomsdomcardi  8352  cardmin2  8379  pm54.43lem  8380  alephgeom  8463  alephval3  8491  pwcdadom  8596  cfsuc  8637  cflim2  8643  alephval2  8947  axunnd  8971  canthp1lem1  9030  pwxpndom2  9043  rankcf  9155  pinq  9305  adderpq  9334  mulerpq  9335  nqpr  9392  ltsopr  9410  ltapr  9423  renepnf  9641  renemnf  9642  lt0ne0d  10118  prodgt0  10387  nnne0  10568  xrltnr  11330  pnfnlt  11337  nltmnf  11338  xrltnsym  11343  nltpnft  11367  ngtmnft  11368  xsubge0  11453  xmullem2  11457  xlemul1a  11480  xrsupsslem  11498  xrinfmsslem  11499  xrub  11503  fzpreddisj  11729  uzinf  12044  hashnemnf  12385  hashclb  12398  hasheq0  12401  hashnn0n0nn  12426  cats1un  12664  geolim  13642  geolim2  13643  georeclim  13644  geoisumr  13650  bitsfzolem  13943  bitsfzo  13944  bitsinv1lem  13950  sadcp1  13964  saddisjlem  13973  smu01lem  13994  3prm  14093  pcgcd1  14259  pc2dvds  14261  pcmpt  14270  prmreclem5  14297  vdwap0  14353  setcepi  15273  oduclatb  15631  cntzrcl  16170  pmtrfrn  16289  pmtrprfval  16318  pmtrprfvalrn  16319  psgnunilem5  16325  odhash3  16402  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzsplit  16747  gsumzsplitOLD  16748  dprdcntz2  16888  0rngnnzr  17716  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  mplrcl  17953  psrbagsn  17959  xrsdsreclblem  18260  dsmmbas2  18563  dsmmfi  18564  islindf4  18668  pmatcollpw3fi1lem1  19082  istps  19232  haust1  19647  hauspwdom  19796  kqcldsat  19997  csdfil  20158  tsmssplit  20417  dscopn  20857  htpycc  21243  pco1  21278  pcohtpylem  21282  pcopt  21285  pcopt2  21286  pcoass  21287  pcorevlem  21289  itg11  21861  bddmulibl  22008  lhop1  22178  deg1nn0clb  22253  plypf1  22372  vieta1lem2  22469  logdmn0  22777  logcnlem3  22781  fsumharmonic  23097  sqff1o  23212  perfectlem1  23260  bposlem5  23319  lgsval2lem  23337  ostth  23580  legso  23740  axlowdimlem13  23961  axlowdimlem16  23964  axlowdim1  23966  axlowdim  23968  umgrafi  24026  rusgranumwlkl1  24651  ex-res  24867  gxnval  24966  norm1exi  25872  dmadjrnb  26529  strlem1  26873  largei  26890  ifeqeqx  27121  ubico  27282  dya2iocuni  27922  eulerpartlemgh  27985  ballotlem4  28105  plymulx0  28172  signswch  28186  signstfvneq0  28197  signlem0  28212  subfacp1lem1  28291  opelco3  28813  wsuclem  28986  sltval2  29021  sltintdifex  29028  sltres  29029  dfrdg4  29205  linedegen  29398  rankeq1o  29433  hfninf  29448  ordcmp  29517  mblfinlem1  29656  diophin  30338  fiphp3d  30385  expdioph  30597  wepwsolem  30619  kelac1  30641  iooinlbub  31126  stoweidlem34  31362  usgedgnlp  31905  bj-projval  33653  bj-inftyexpidisj  33703  elpadd0  34623
  Copyright terms: Public domain W3C validator