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

Theorem mtbiri 304
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 210 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 181 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  psstr  3569  n0i  3766  sbcel12  3802  sbcel2  3808  sbcbr123  4475  axnul  4553  axnulOLD  4554  intex  4580  intnex  4581  iin0  4598  nfcvb  4651  opelopabsb  4730  0nelelxp  4882  elimasni  5214  0ellim  5504  onxpdisj  5561  ndmfvrcl  5906  canth  6264  brabv  6350  oprssdm  6464  ndmovrcl  6469  omelon2  6718  undefnel2  7035  tfr2b  7125  tz7.44-3  7137  omeulem1  7294  eceqoveq  7479  2dom  7652  omxpenlem  7682  domunsn  7731  disjen  7738  infensuc  7759  snnen2o  7770  elfi2  7937  en3lp  8130  preleq  8131  rankxpsuc  8361  sdomsdomcardi  8413  cardmin2  8440  pm54.43lem  8441  alephgeom  8520  alephval3  8548  pwcdadom  8653  cfsuc  8694  cflim2  8700  alephval2  9004  axunnd  9028  canthp1lem1  9084  pwxpndom2  9097  rankcf  9209  pinq  9359  adderpq  9388  mulerpq  9389  nqpr  9446  ltsopr  9464  ltapr  9477  renepnf  9695  renemnf  9696  lt0ne0d  10186  prodgt0  10457  nnne0  10649  xrltnr  11428  pnfnlt  11437  nltmnf  11438  xrltnsym  11443  nltpnft  11468  ngtmnft  11469  xsubge0  11554  xmullem2  11558  xlemul1a  11581  xrsupsslem  11599  xrinfmsslem  11600  xrub  11604  fzpreddisj  11852  fzm1  11881  uzinf  12185  hashnemnf  12533  hashclb  12546  hasheq0  12550  hashnn0n0nn  12576  lsw0  12716  cats1un  12834  geolim  13925  geolim2  13926  georeclim  13927  geoisumr  13933  bitsfzolem  14406  bitsfzolemOLD  14407  bitsfzo  14408  bitsinv1lem  14414  sadcp1  14428  saddisjlem  14437  smu01lem  14458  3prm  14640  pcgcd1  14825  pc2dvds  14827  pcmpt  14836  prmreclem5  14863  vdwap0  14925  setcepi  15982  oduclatb  16389  cntzrcl  16980  pmtrfrn  17098  pmtrprfval  17127  pmtrprfvalrn  17128  psgnunilem5  17134  odhash3  17224  gsumzaddlem  17553  gsumzsplit  17559  dprdcntz2  17670  0ringnnzr  18492  mplcoe1  18688  mplcoe5  18691  psrbagsn  18717  xrsdsreclblem  19013  dsmmbas2  19298  dsmmfi  19299  islindf4  19394  pmatcollpw3fi1lem1  19808  istps  19949  haust1  20366  hauspwdom  20514  kqcldsat  20746  csdfil  20907  tsmssplit  21164  dscopn  21586  htpycc  22009  pco1  22044  pcohtpylem  22048  pcopt  22051  pcopt2  22052  pcoass  22053  pcorevlem  22055  itg11  22647  bddmulibl  22794  lhop1  22964  deg1nn0clb  23037  plypf1  23164  vieta1lem2  23262  logdmn0  23583  logcnlem3  23587  fsumharmonic  23935  sqff1o  24107  perfectlem1  24155  bposlem5  24214  lgsval2lem  24232  ostth  24475  legso  24642  axlowdimlem13  24982  axlowdimlem16  24985  axlowdim1  24987  axlowdim  24989  umgrafi  25047  rusgranumwlkl1  25673  ex-res  25889  gxnval  25986  norm1exi  26901  dmadjrnb  27557  strlem1  27901  largei  27918  ifeqeqx  28160  ubico  28363  dya2iocuni  29113  eulerpartlemgh  29219  ballotlem4  29339  plymulx0  29444  signswch  29458  signstfvneq0  29469  signlem0  29484  subfacp1lem1  29910  bcneg1  30379  opelco3  30427  wsuclem  30515  sltval2  30550  sltintdifex  30557  sltres  30558  dfrdg4  30723  linedegen  30915  rankeq1o  30943  hfninf  30958  ordcmp  31112  bj-projval  31558  bj-inftyexpidisj  31616  relowlpssretop  31731  finxpreclem2  31746  finxpreclem3  31749  finxpreclem5  31751  poimirlem18  31922  poimirlem19  31923  poimirlem20  31924  mblfinlem1  31941  elpadd0  33343  diophin  35584  fiphp3d  35631  expdioph  35848  wepwsolem  35870  kelac1  35891  relintabex  36157  brnonrel  36165  relexp01min  36275  iooinlbub  37547  stoweidlem34  37835  fourierdlem60  37970  fourierdlem61  37971  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  umgrfi  39011  uvtxa01vtx  39229  usgedgnlp  39342  dig2nn1st  40038
  Copyright terms: Public domain W3C validator