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

Theorem mtbiri 309
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 212 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 183 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  psstr  3505  n0i  3704  sbcel12  3740  sbcel2  3746  sbcbr123  4426  axnul  4504  axnulOLD  4505  intex  4532  intnex  4533  iin0  4550  nfcvb  4603  opelopabsb  4684  0nelelxp  4841  elimasni  5173  0ellim  5464  onxpdisj  5521  ndmfvrcl  5873  canth  6235  brabv  6323  oprssdm  6438  ndmovrcl  6443  omelon2  6692  undefnel2  7011  tfr2b  7101  tz7.44-3  7113  omeulem1  7270  eceqoveq  7455  2dom  7629  omxpenlem  7660  domunsn  7709  disjen  7716  infensuc  7737  snnen2o  7748  elfi2  7915  en3lp  8108  preleq  8109  rankxpsuc  8340  sdomsdomcardi  8392  cardmin2  8419  pm54.43lem  8420  alephgeom  8500  alephval3  8528  pwcdadom  8633  cfsuc  8674  cflim2  8680  alephval2  8984  axunnd  9008  canthp1lem1  9064  pwxpndom2  9077  rankcf  9189  pinq  9339  adderpq  9368  mulerpq  9369  nqpr  9426  ltsopr  9444  ltapr  9457  renepnf  9675  renemnf  9676  lt0ne0d  10168  prodgt0  10439  nnne0  10631  xrltnr  11411  pnfnlt  11420  nltmnf  11421  xrltnsym  11426  nltpnft  11451  ngtmnft  11452  xsubge0  11537  xmullem2  11541  xlemul1a  11564  xrsupsslem  11582  xrinfmsslem  11583  xrub  11587  fzpreddisj  11836  fzm1  11865  uzinf  12173  hashnemnf  12521  hashclb  12534  hasheq0  12538  hashnn0n0nn  12564  lsw0  12710  cats1un  12831  geolim  13937  geolim2  13938  georeclim  13939  geoisumr  13945  bitsfzolem  14418  bitsfzolemOLD  14419  bitsfzo  14420  bitsinv1lem  14426  sadcp1  14440  saddisjlem  14449  smu01lem  14470  3prm  14652  pcgcd1  14837  pc2dvds  14839  pcmpt  14848  prmreclem5  14875  vdwap0  14937  setcepi  15994  oduclatb  16401  cntzrcl  16992  pmtrfrn  17110  pmtrprfval  17139  pmtrprfvalrn  17140  psgnunilem5  17146  odhash3  17236  gsumzaddlem  17565  gsumzsplit  17571  dprdcntz2  17682  0ringnnzr  18504  mplcoe1  18700  mplcoe5  18703  psrbagsn  18729  xrsdsreclblem  19025  dsmmbas2  19311  dsmmfi  19312  islindf4  19407  pmatcollpw3fi1lem1  19821  istps  19962  haust1  20379  hauspwdom  20527  kqcldsat  20759  csdfil  20920  tsmssplit  21177  dscopn  21599  htpycc  22022  pco1  22057  pcohtpylem  22061  pcopt  22064  pcopt2  22065  pcoass  22066  pcorevlem  22068  itg11  22661  bddmulibl  22808  lhop1  22978  deg1nn0clb  23051  plypf1  23178  vieta1lem2  23276  logdmn0  23597  logcnlem3  23601  fsumharmonic  23949  sqff1o  24121  perfectlem1  24169  bposlem5  24228  lgsval2lem  24246  ostth  24489  legso  24656  axlowdimlem13  24996  axlowdimlem16  24999  axlowdim1  25001  axlowdim  25003  umgrafi  25061  rusgranumwlkl1  25687  ex-res  25903  gxnval  26000  norm1exi  26915  dmadjrnb  27571  strlem1  27915  largei  27932  ifeqeqx  28169  ubico  28365  dya2iocuni  29111  eulerpartlemgh  29217  ballotlem4  29337  plymulx0  29442  signswch  29456  signstfvneq0  29467  signlem0  29482  subfacp1lem1  29908  bcneg1  30378  opelco3  30426  wsuclem  30514  sltval2  30549  sltintdifex  30556  sltres  30557  dfrdg4  30724  linedegen  30916  rankeq1o  30944  hfninf  30959  ordcmp  31113  bj-projval  31592  bj-inftyexpidisj  31654  relowlpssretop  31769  finxpreclem2  31784  finxpreclem3  31787  finxpreclem5  31789  poimirlem18  31960  poimirlem19  31961  poimirlem20  31962  mblfinlem1  31979  elpadd0  33376  diophin  35617  fiphp3d  35664  expdioph  35880  wepwsolem  35902  kelac1  35923  relintabex  36189  brnonrel  36197  relexp01min  36307  iooinlbub  37639  stoweidlem34  37952  fourierdlem60  38087  fourierdlem61  38088  nnsum4primeseven  38986  nnsum4primesevenALTV  38987  prprrab  39166  nn0nepnf  39177  upgrfi  39282  uvtxa01vtx  39572  usgedgnlp  40047  dig2nn1st  40741
  Copyright terms: Public domain W3C validator