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

Theorem mtbiri 301
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  3594  n0i  3788  sbcel12  3822  sbcel2  3828  sbcbr123  4490  axnul  4567  intex  4593  intnex  4594  iin0  4611  nfcvb  4667  opelopabsb  4746  0ellim  4929  0nelelxp  5017  onxpdisj  5071  elimasni  5352  ndmfvrcl  5873  canth  6229  brabv  6315  oprssdm  6429  ndmovrcl  6434  omelon2  6685  undefnel2  6998  tfr2b  7057  tz7.44-3  7066  omeulem1  7223  eceqoveq  7408  2dom  7581  omxpenlem  7611  domunsn  7660  disjen  7667  infensuc  7688  snnen2o  7699  elfi2  7866  en3lp  8024  preleq  8025  rankxpsuc  8291  sdomsdomcardi  8343  cardmin2  8370  pm54.43lem  8371  alephgeom  8454  alephval3  8482  pwcdadom  8587  cfsuc  8628  cflim2  8634  alephval2  8938  axunnd  8962  canthp1lem1  9019  pwxpndom2  9032  rankcf  9144  pinq  9294  adderpq  9323  mulerpq  9324  nqpr  9381  ltsopr  9399  ltapr  9412  renepnf  9630  renemnf  9631  lt0ne0d  10114  prodgt0  10383  nnne0  10564  xrltnr  11333  pnfnlt  11340  nltmnf  11341  xrltnsym  11346  nltpnft  11370  ngtmnft  11371  xsubge0  11456  xmullem2  11460  xlemul1a  11483  xrsupsslem  11501  xrinfmsslem  11502  xrub  11506  fzpreddisj  11733  fzm1  11762  uzinf  12058  hashnemnf  12399  hashclb  12412  hasheq0  12416  hashnn0n0nn  12442  lsw0  12574  cats1un  12692  geolim  13761  geolim2  13762  georeclim  13763  geoisumr  13769  bitsfzolem  14168  bitsfzo  14169  bitsinv1lem  14175  sadcp1  14189  saddisjlem  14198  smu01lem  14219  3prm  14318  pcgcd1  14484  pc2dvds  14486  pcmpt  14495  prmreclem5  14522  vdwap0  14578  setcepi  15566  oduclatb  15973  cntzrcl  16564  pmtrfrn  16682  pmtrprfval  16711  pmtrprfvalrn  16712  psgnunilem5  16718  odhash3  16795  gsumzaddlem  17133  gsumzaddlemOLD  17135  gsumzsplit  17143  gsumzsplitOLD  17144  dprdcntz2  17281  0ringnnzr  18112  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  psrbagsn  18355  xrsdsreclblem  18659  dsmmbas2  18941  dsmmfi  18942  islindf4  19040  pmatcollpw3fi1lem1  19454  istps  19604  haust1  20020  hauspwdom  20168  kqcldsat  20400  csdfil  20561  tsmssplit  20820  dscopn  21260  htpycc  21646  pco1  21681  pcohtpylem  21685  pcopt  21688  pcopt2  21689  pcoass  21690  pcorevlem  21692  itg11  22264  bddmulibl  22411  lhop1  22581  deg1nn0clb  22656  plypf1  22775  vieta1lem2  22873  logdmn0  23189  logcnlem3  23193  fsumharmonic  23539  sqff1o  23654  perfectlem1  23702  bposlem5  23761  lgsval2lem  23779  ostth  24022  legso  24186  axlowdimlem13  24459  axlowdimlem16  24462  axlowdim1  24464  axlowdim  24466  umgrafi  24524  rusgranumwlkl1  25149  ex-res  25364  gxnval  25460  norm1exi  26366  dmadjrnb  27023  strlem1  27367  largei  27384  ifeqeqx  27625  ubico  27820  dya2iocuni  28491  eulerpartlemgh  28581  ballotlem4  28701  plymulx0  28768  signswch  28782  signstfvneq0  28793  signlem0  28808  subfacp1lem1  28887  opelco3  29448  wsuclem  29621  sltval2  29656  sltintdifex  29663  sltres  29664  dfrdg4  29828  linedegen  30021  rankeq1o  30056  hfninf  30071  ordcmp  30140  mblfinlem1  30291  diophin  30945  fiphp3d  30992  expdioph  31204  wepwsolem  31226  kelac1  31248  iooinlbub  31773  stoweidlem34  32055  fourierdlem60  32188  fourierdlem61  32189  usgedgnlp  32782  dig2nn1st  33480  bj-projval  34955  bj-inftyexpidisj  35013  elpadd0  35930  relexp01min  38219
  Copyright terms: Public domain W3C validator