MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbiri Structured version   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  |-  -.  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  3457  n0i  3639  sbcel2  3680  sbcbr123  4340  axnul  4417  intex  4445  intnex  4446  iin0  4463  nfcvb  4519  opelopabsb  4597  0ellim  4777  0nelelxp  4864  onxpdisj  4916  elimasni  5193  ndmfvrcl  5712  canth  6046  brabv  6131  oprssdm  6243  ndmovrcl  6248  omelon2  6487  undefnel2  6792  tfr2b  6851  tz7.44-3  6860  omeulem1  7017  eceqoveq  7201  2dom  7378  omxpenlem  7408  domunsn  7457  disjen  7464  infensuc  7485  elfi2  7660  sucprcregOLD  7811  en3lp  7818  preleq  7819  rankxpsuc  8085  sdomsdomcardi  8137  cardmin2  8164  pm54.43lem  8165  alephgeom  8248  alephval3  8276  pwcdadom  8381  cfsuc  8422  cflim2  8428  alephval2  8732  axunnd  8756  canthp1lem1  8815  pwxpndom2  8828  rankcf  8940  pinq  9092  adderpq  9121  mulerpq  9122  nqpr  9179  ltsopr  9197  ltapr  9210  renepnf  9427  renemnf  9428  lt0ne0d  9901  prodgt0  10170  nnne0  10350  xrltnr  11097  pnfnlt  11104  nltmnf  11105  xrltnsym  11110  nltpnft  11134  ngtmnft  11135  xsubge0  11220  xmullem2  11224  xlemul1a  11247  xrsupsslem  11265  xrinfmsslem  11266  xrub  11270  fzpreddisj  11500  uzinf  11784  hashnemnf  12111  hashclb  12124  hasheq0  12127  hashnn0n0nn  12149  cats1un  12366  geolim  13326  geolim2  13327  georeclim  13328  geoisumr  13334  bitsfzolem  13626  bitsfzo  13627  bitsinv1lem  13633  sadcp1  13647  saddisjlem  13656  smu01lem  13677  3prm  13776  pcgcd1  13939  pc2dvds  13941  pcmpt  13950  prmreclem5  13977  vdwap0  14033  setcepi  14952  oduclatb  15310  cntzrcl  15838  pmtrfrn  15957  pmtrprfval  15986  pmtrprfvalrn  15987  psgnunilem5  15993  odhash3  16068  gsumzaddlem  16401  gsumzaddlemOLD  16403  gsumzsplit  16411  gsumzsplitOLD  16412  dprdcntz2  16526  mplcoe1  17522  mplcoe2  17525  mplcoe2OLD  17526  mplrcl  17547  psrbagsn  17553  strov2rcl  17667  xrsdsreclblem  17818  dsmmbas2  18121  dsmmfi  18122  islindf4  18226  istps  18500  haust1  18915  hauspwdom  19064  kqcldsat  19265  csdfil  19426  tsmssplit  19685  dscopn  20125  htpycc  20511  pco1  20546  pcohtpylem  20550  pcopt  20553  pcopt2  20554  pcoass  20555  pcorevlem  20557  itg11  21128  bddmulibl  21275  lhop1  21445  deg1nn0clb  21520  plypf1  21639  vieta1lem2  21736  logdmn0  22044  logcnlem3  22048  fsumharmonic  22364  sqff1o  22479  perfectlem1  22527  bposlem5  22586  lgsval2lem  22604  ostth  22847  axlowdimlem13  23135  axlowdimlem16  23138  axlowdim1  23140  axlowdim  23142  umgrafi  23191  ex-res  23583  gxnval  23682  norm1exi  24588  dmadjrnb  25245  strlem1  25589  largei  25606  ifeqeqx  25837  ubico  25998  dya2iocuni  26634  eulerpartlemgh  26691  ballotlem4  26811  plymulx0  26878  signswch  26892  signstfvneq0  26903  signlem0  26918  subfacp1lem1  26997  opelco3  27518  wsuclem  27691  sltval2  27726  sltintdifex  27733  sltres  27734  dfrdg4  27910  linedegen  28103  rankeq1o  28138  hfninf  28153  ordcmp  28223  mblfinlem1  28353  diophin  29036  fiphp3d  29083  expdioph  29297  wepwsolem  29319  kelac1  29341  stoweidlem34  29754  rusgranumwlkl1  30484  snnen2o  30662  0rngnnzr  30695  bj-projval  32219  bj-inftyexpidisj  32262  elpadd0  33175
  Copyright terms: Public domain W3C validator