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  3280  n0i  3460  axnul  4148  intex  4167  intnex  4168  iin0  4184  nfcvb  4205  opelopabsb  4275  0ellim  4454  omelon2  4668  0nelelxp  4718  onxpdisj  4769  elimasni  5040  ndmfvrcl  5553  oprssdm  6002  ndmovrcl  6006  canth  6294  undefnel2  6302  tfr2b  6412  tz7.44-3  6421  omeulem1  6580  eceqoveq  6763  2dom  6933  omxpenlem  6963  domunsn  7011  disjen  7018  infensuc  7039  elfi2  7168  sucprcreg  7313  preleq  7318  en3lp  7418  rankxpsuc  7552  sdomsdomcardi  7604  cardmin2  7631  pm54.43lem  7632  alephgeom  7709  alephval3  7737  pwcdadom  7842  cfsuc  7883  cflim2  7889  alephval2  8194  axunnd  8218  canthp1lem1  8274  pwxpndom2  8287  rankcf  8399  pinq  8551  adderpq  8580  mulerpq  8581  nqpr  8638  ltsopr  8656  ltapr  8669  renepnf  8879  renemnf  8880  lt0ne0d  9338  prodgt0  9601  nnne0  9778  xrltnr  10462  pnfnlt  10467  nltmnf  10468  xrltnsym  10471  nltpnft  10495  ngtmnft  10496  xsubge0  10581  xmullem2  10585  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  uzinf  11028  hashclb  11352  hasheq0  11353  cats1un  11476  geolim  12326  geolim2  12327  georeclim  12328  geoisumr  12334  bitsfzolem  12625  bitsfzo  12626  bitsinv1lem  12632  sadcp1  12646  saddisjlem  12655  smu01lem  12676  3prm  12775  pcgcd1  12929  pc2dvds  12931  pcmpt  12940  prmreclem5  12967  vdwap0  13023  setcepi  13920  oduclatb  14248  cntzrcl  14803  odhash3  14887  gsumzaddlem  15203  gsumzsplit  15206  dprdcntz2  15273  mplcoe1  16209  mplcoe2  16211  mplrcl  16231  psrbagsn  16236  strov2rcl  16315  xrsdsreclblem  16417  istps  16674  haust1  17080  hauspwdom  17227  kqcldsat  17424  csdfil  17589  tsmssplit  17834  dscopn  18096  htpycc  18478  pco1  18513  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  itg11  19046  bddmulibl  19193  lhop1  19361  deg1nn0clb  19476  plypf1  19594  vieta1lem2  19691  logdmn0  19987  logcnlem3  19991  fsumharmonic  20305  sqff1o  20420  perfectlem1  20468  bposlem5  20527  lgsval2lem  20545  ostth  20788  ex-res  20828  gxnval  20927  norm1exi  21829  dmadjrnb  22486  strlem1  22830  largei  22847  ifeqeqx  23034  ballotlem4  23057  ubico  23268  subfacp1lem1  23710  umgrafi  23874  sltval2  24310  sltintdifex  24317  sltres  24318  funpartfv  24483  dfrdg4  24488  axlowdimlem13  24582  axlowdimlem16  24585  axlowdim1  24587  axlowdim  24589  linedegen  24766  rankeq1o  24801  hfninf  24816  ordcmp  24886  diophin  26852  fiphp3d  26902  expdioph  27116  wepwsolem  27138  kelac1  27161  dsmmbas2  27203  dsmmfi  27204  uvcff  27240  islindf4  27308  pmtrfrn  27400  psgnunilem5  27417  stoweidlem34  27783  elpadd0  29998
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