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

Theorem mtbiri 295
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 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 171 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  psstr  3411  n0i  3593  axnul  4297  intex  4316  intnex  4317  iin0  4333  nfcvb  4354  opelopabsb  4425  0ellim  4603  omelon2  4816  0nelelxp  4866  onxpdisj  4916  elimasni  5190  ndmfvrcl  5715  brabv  6079  oprssdm  6187  ndmovrcl  6192  canth  6498  undefnel2  6506  tfr2b  6616  tz7.44-3  6625  omeulem1  6784  eceqoveq  6968  2dom  7138  omxpenlem  7168  domunsn  7216  disjen  7223  infensuc  7244  elfi2  7377  sucprcreg  7523  preleq  7528  en3lp  7628  rankxpsuc  7762  sdomsdomcardi  7814  cardmin2  7841  pm54.43lem  7842  alephgeom  7919  alephval3  7947  pwcdadom  8052  cfsuc  8093  cflim2  8099  alephval2  8403  axunnd  8427  canthp1lem1  8483  pwxpndom2  8496  rankcf  8608  pinq  8760  adderpq  8789  mulerpq  8790  nqpr  8847  ltsopr  8865  ltapr  8878  renepnf  9088  renemnf  9089  lt0ne0d  9548  prodgt0  9811  nnne0  9988  xrltnr  10676  pnfnlt  10681  nltmnf  10682  xrltnsym  10686  nltpnft  10710  ngtmnft  10711  xsubge0  10796  xmullem2  10800  xlemul1a  10823  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  uzinf  11260  hashnemnf  11583  hashclb  11596  hasheq0  11599  hashnn0n0nn  11619  cats1un  11745  geolim  12602  geolim2  12603  georeclim  12604  geoisumr  12610  bitsfzolem  12901  bitsfzo  12902  bitsinv1lem  12908  sadcp1  12922  saddisjlem  12931  smu01lem  12952  3prm  13051  pcgcd1  13205  pc2dvds  13207  pcmpt  13216  prmreclem5  13243  vdwap0  13299  setcepi  14198  oduclatb  14526  cntzrcl  15081  odhash3  15165  gsumzaddlem  15481  gsumzsplit  15484  dprdcntz2  15551  mplcoe1  16483  mplcoe2  16485  mplrcl  16505  psrbagsn  16510  strov2rcl  16586  xrsdsreclblem  16699  istps  16956  haust1  17370  hauspwdom  17517  kqcldsat  17718  csdfil  17879  tsmssplit  18134  dscopn  18574  htpycc  18958  pco1  18993  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  itg11  19536  bddmulibl  19683  lhop1  19851  deg1nn0clb  19966  plypf1  20084  vieta1lem2  20181  logdmn0  20484  logcnlem3  20488  fsumharmonic  20803  sqff1o  20918  perfectlem1  20966  bposlem5  21025  lgsval2lem  21043  ostth  21286  umgrafi  21310  ex-res  21702  gxnval  21801  norm1exi  22705  dmadjrnb  23362  strlem1  23706  largei  23723  ifeqeqx  23954  ubico  24091  dya2iocuni  24586  ballotlem4  24709  subfacp1lem1  24818  sltval2  25524  sltintdifex  25531  sltres  25532  dfrdg4  25703  axlowdimlem13  25797  axlowdimlem16  25800  axlowdim1  25802  axlowdim  25804  linedegen  25981  rankeq1o  26016  hfninf  26031  ordcmp  26101  mblfinlem  26143  diophin  26721  fiphp3d  26770  expdioph  26984  wepwsolem  27006  kelac1  27029  dsmmbas2  27071  dsmmfi  27072  uvcff  27108  islindf4  27176  pmtrfrn  27268  psgnunilem5  27285  stoweidlem34  27650  elpadd0  30291
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator