MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbiri 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
mtbiri.maj
Assertion
Ref Expression
mtbiri

Proof of Theorem mtbiri
StepHypRef Expression
1 mtbiri.min . 2
2 mtbiri.maj . . 3
32biimpd 207 . 2
41, 3mtoi 178 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  psstr  3607  n0i  3789  sbcel12  3823  sbcel2  3831  sbcbr123  4503  axnul  4580  intex  4608  intnex  4609  iin0  4626  nfcvb  4682  opelopabsb  4762  0ellim  4945  0nelelxp  5033  onxpdisj  5088  elimasni  5369  ndmfvrcl  5896  canth  6254  brabv  6342  oprssdm  6456  ndmovrcl  6461  omelon2  6712  undefnel2  7025  tfr2b  7084  tz7.44-3  7093  omeulem1  7250  eceqoveq  7435  2dom  7608  omxpenlem  7638  domunsn  7687  disjen  7694  infensuc  7715  snnen2o  7726  elfi2  7894  sucprcregOLD  8047  en3lp  8054  preleq  8055  rankxpsuc  8321  sdomsdomcardi  8373  cardmin2  8400  pm54.43lem  8401  alephgeom  8484  alephval3  8512  pwcdadom  8617  cfsuc  8658  cflim2  8664  alephval2  8968  axunnd  8992  canthp1lem1  9051  pwxpndom2  9064  rankcf  9176  pinq  9326  adderpq  9355  mulerpq  9356  nqpr  9413  ltsopr  9431  ltapr  9444  renepnf  9662  renemnf  9663  lt0ne0d  10143  prodgt0  10412  nnne0  10593  xrltnr  11359  pnfnlt  11366  nltmnf  11367  xrltnsym  11372  nltpnft  11396  ngtmnft  11397  xsubge0  11482  xmullem2  11486  xlemul1a  11509  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  fzpreddisj  11758  fzm1  11787  uzinf  12076  hashnemnf  12417  hashclb  12430  hasheq0  12433  hashnn0n0nn  12458  cats1un  12701  geolim  13679  geolim2  13680  georeclim  13681  geoisumr  13687  bitsfzolem  14084  bitsfzo  14085  bitsinv1lem  14091  sadcp1  14105  saddisjlem  14114  smu01lem  14135  3prm  14234  pcgcd1  14400  pc2dvds  14402  pcmpt  14411  prmreclem5  14438  vdwap0  14494  setcepi  15415  oduclatb  15774  cntzrcl  16365  pmtrfrn  16483  pmtrprfval  16512  pmtrprfvalrn  16513  psgnunilem5  16519  odhash3  16596  gsumzaddlem  16934  gsumzaddlemOLD  16936  gsumzsplit  16944  gsumzsplitOLD  16945  dprdcntz2  17086  0ringnnzr  17917  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  psrbagsn  18160  xrsdsreclblem  18464  dsmmbas2  18768  dsmmfi  18769  islindf4  18873  pmatcollpw3fi1lem1  19287  istps  19437  haust1  19853  hauspwdom  20002  kqcldsat  20234  csdfil  20395  tsmssplit  20654  dscopn  21094  htpycc  21480  pco1  21515  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  itg11  22098  bddmulibl  22245  lhop1  22415  deg1nn0clb  22490  plypf1  22609  vieta1lem2  22707  logdmn0  23021  logcnlem3  23025  fsumharmonic  23341  sqff1o  23456  perfectlem1  23504  bposlem5  23563  lgsval2lem  23581  ostth  23824  legso  23985  axlowdimlem13  24257  axlowdimlem16  24260  axlowdim1  24262  axlowdim  24264  umgrafi  24322  rusgranumwlkl1  24947  ex-res  25162  gxnval  25262  norm1exi  26168  dmadjrnb  26825  strlem1  27169  largei  27186  ifeqeqx  27419  ubico  27586  dya2iocuni  28254  eulerpartlemgh  28317  ballotlem4  28437  plymulx0  28504  signswch  28518  signstfvneq0  28529  signlem0  28544  subfacp1lem1  28623  opelco3  29208  wsuclem  29381  sltval2  29416  sltintdifex  29423  sltres  29424  dfrdg4  29600  linedegen  29793  rankeq1o  29828  hfninf  29843  ordcmp  29912  mblfinlem1  30051  diophin  30706  fiphp3d  30753  expdioph  30965  wepwsolem  30987  kelac1  31009  iooinlbub  31534  stoweidlem34  31816  fourierdlem60  31949  fourierdlem61  31950  usgedgnlp  32410  bj-projval  34554  bj-inftyexpidisj  34613  elpadd0  35533
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
  Copyright terms: Public domain W3C validator