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

Theorem mtbiri 294
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 198 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 169 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  psstr  3293  n0i  3473  axnul  4164  intex  4183  intnex  4184  iin0  4200  nfcvb  4221  opelopabsb  4291  0ellim  4470  omelon2  4684  0nelelxp  4734  onxpdisj  4785  elimasni  5056  ndmfvrcl  5569  oprssdm  6018  ndmovrcl  6022  canth  6310  undefnel2  6318  tfr2b  6428  tz7.44-3  6437  omeulem1  6596  eceqoveq  6779  2dom  6949  omxpenlem  6979  domunsn  7027  disjen  7034  infensuc  7055  elfi2  7184  sucprcreg  7329  preleq  7334  en3lp  7434  rankxpsuc  7568  sdomsdomcardi  7620  cardmin2  7647  pm54.43lem  7648  alephgeom  7725  alephval3  7753  pwcdadom  7858  cfsuc  7899  cflim2  7905  alephval2  8210  axunnd  8234  canthp1lem1  8290  pwxpndom2  8303  rankcf  8415  pinq  8567  adderpq  8596  mulerpq  8597  nqpr  8654  ltsopr  8672  ltapr  8685  renepnf  8895  renemnf  8896  lt0ne0d  9354  prodgt0  9617  nnne0  9794  xrltnr  10478  pnfnlt  10483  nltmnf  10484  xrltnsym  10487  nltpnft  10511  ngtmnft  10512  xsubge0  10597  xmullem2  10601  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  uzinf  11044  hashclb  11368  hasheq0  11369  cats1un  11492  geolim  12342  geolim2  12343  georeclim  12344  geoisumr  12350  bitsfzolem  12641  bitsfzo  12642  bitsinv1lem  12648  sadcp1  12662  saddisjlem  12671  smu01lem  12692  3prm  12791  pcgcd1  12945  pc2dvds  12947  pcmpt  12956  prmreclem5  12983  vdwap0  13039  setcepi  13936  oduclatb  14264  cntzrcl  14819  odhash3  14903  gsumzaddlem  15219  gsumzsplit  15222  dprdcntz2  15289  mplcoe1  16225  mplcoe2  16227  mplrcl  16247  psrbagsn  16252  strov2rcl  16331  xrsdsreclblem  16433  istps  16690  haust1  17096  hauspwdom  17243  kqcldsat  17440  csdfil  17605  tsmssplit  17850  dscopn  18112  htpycc  18494  pco1  18529  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  itg11  19062  bddmulibl  19209  lhop1  19377  deg1nn0clb  19492  plypf1  19610  vieta1lem2  19707  logdmn0  20003  logcnlem3  20007  fsumharmonic  20321  sqff1o  20436  perfectlem1  20484  bposlem5  20543  lgsval2lem  20561  ostth  20804  ex-res  20844  gxnval  20943  norm1exi  21845  dmadjrnb  22502  strlem1  22846  largei  22863  ifeqeqx  23050  ballotlem4  23073  ubico  23283  subfacp1lem1  23725  umgrafi  23889  sltval2  24381  sltintdifex  24388  sltres  24389  dfrdg4  24560  axlowdimlem13  24654  axlowdimlem16  24657  axlowdim1  24659  axlowdim  24661  linedegen  24838  rankeq1o  24873  hfninf  24888  ordcmp  24958  diophin  26955  fiphp3d  27005  expdioph  27219  wepwsolem  27241  kelac1  27264  dsmmbas2  27306  dsmmfi  27307  uvcff  27343  islindf4  27411  pmtrfrn  27503  psgnunilem5  27520  stoweidlem34  27886  brabv  28193  elpadd0  30620
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 177
  Copyright terms: Public domain W3C validator