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  3575  n0i  3772  sbcel12  3806  sbcel2  3812  sbcbr123  4477  axnul  4555  intex  4581  intnex  4582  iin0  4599  nfcvb  4652  opelopabsb  4731  0nelelxp  4883  elimasni  5215  0ellim  5504  onxpdisj  5561  ndmfvrcl  5906  canth  6264  brabv  6350  oprssdm  6464  ndmovrcl  6469  omelon2  6718  undefnel2  7032  tfr2b  7122  tz7.44-3  7134  omeulem1  7291  eceqoveq  7476  2dom  7649  omxpenlem  7679  domunsn  7728  disjen  7735  infensuc  7756  snnen2o  7767  elfi2  7934  en3lp  8121  preleq  8122  rankxpsuc  8352  sdomsdomcardi  8404  cardmin2  8431  pm54.43lem  8432  alephgeom  8511  alephval3  8539  pwcdadom  8644  cfsuc  8685  cflim2  8691  alephval2  8995  axunnd  9019  canthp1lem1  9076  pwxpndom2  9089  rankcf  9201  pinq  9351  adderpq  9380  mulerpq  9381  nqpr  9438  ltsopr  9456  ltapr  9469  renepnf  9687  renemnf  9688  lt0ne0d  10178  prodgt0  10449  nnne0  10642  xrltnr  11421  pnfnlt  11430  nltmnf  11431  xrltnsym  11436  nltpnft  11461  ngtmnft  11462  xsubge0  11547  xmullem2  11551  xlemul1a  11574  xrsupsslem  11592  xrinfmsslem  11593  xrub  11597  fzpreddisj  11843  fzm1  11872  uzinf  12176  hashnemnf  12524  hashclb  12537  hasheq0  12541  hashnn0n0nn  12567  lsw0  12699  cats1un  12817  geolim  13904  geolim2  13905  georeclim  13906  geoisumr  13912  bitsfzolem  14382  bitsfzo  14383  bitsinv1lem  14389  sadcp1  14403  saddisjlem  14412  smu01lem  14433  3prm  14612  pcgcd1  14789  pc2dvds  14791  pcmpt  14800  prmreclem5  14827  vdwap0  14889  setcepi  15934  oduclatb  16341  cntzrcl  16932  pmtrfrn  17050  pmtrprfval  17079  pmtrprfvalrn  17080  psgnunilem5  17086  odhash3  17163  gsumzaddlem  17489  gsumzsplit  17495  dprdcntz2  17606  0ringnnzr  18428  mplcoe1  18624  mplcoe5  18627  psrbagsn  18653  xrsdsreclblem  18949  dsmmbas2  19231  dsmmfi  19232  islindf4  19327  pmatcollpw3fi1lem1  19741  istps  19882  haust1  20299  hauspwdom  20447  kqcldsat  20679  csdfil  20840  tsmssplit  21097  dscopn  21519  htpycc  21904  pco1  21939  pcohtpylem  21943  pcopt  21946  pcopt2  21947  pcoass  21948  pcorevlem  21950  itg11  22526  bddmulibl  22673  lhop1  22843  deg1nn0clb  22916  plypf1  23034  vieta1lem2  23132  logdmn0  23450  logcnlem3  23454  fsumharmonic  23802  sqff1o  23972  perfectlem1  24020  bposlem5  24079  lgsval2lem  24097  ostth  24340  legso  24504  axlowdimlem13  24830  axlowdimlem16  24833  axlowdim1  24835  axlowdim  24837  umgrafi  24895  rusgranumwlkl1  25520  ex-res  25736  gxnval  25833  norm1exi  26738  dmadjrnb  27394  strlem1  27738  largei  27755  ifeqeqx  27997  ubico  28193  dya2iocuni  28944  eulerpartlemgh  29037  ballotlem4  29157  plymulx0  29224  signswch  29238  signstfvneq0  29249  signlem0  29264  subfacp1lem1  29690  bcneg1  30159  opelco3  30207  wsuclem  30295  sltval2  30330  sltintdifex  30337  sltres  30338  dfrdg4  30503  linedegen  30695  rankeq1o  30723  hfninf  30738  ordcmp  30892  bj-projval  31339  bj-inftyexpidisj  31397  relowlpssretop  31501  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  mblfinlem1  31681  elpadd0  33083  diophin  35324  fiphp3d  35371  expdioph  35584  wepwsolem  35606  kelac1  35627  relexp01min  35944  iooinlbub  37183  stoweidlem34  37464  fourierdlem60  37598  fourierdlem61  37599  nnsum4primeseven  38285  nnsum4primesevenALTV  38286  usgedgnlp  38480  dig2nn1st  39177
  Copyright terms: Public domain W3C validator