MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbiri Structured version   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  3451  n0i  3633  axnul  4337  intex  4356  intnex  4357  iin0  4373  nfcvb  4394  opelopabsb  4465  0ellim  4643  omelon2  4857  0nelelxp  4907  onxpdisj  4957  elimasni  5231  ndmfvrcl  5756  brabv  6120  oprssdm  6228  ndmovrcl  6233  canth  6539  undefnel2  6547  tfr2b  6657  tz7.44-3  6666  omeulem1  6825  eceqoveq  7009  2dom  7179  omxpenlem  7209  domunsn  7257  disjen  7264  infensuc  7285  elfi2  7419  sucprcreg  7567  preleq  7572  en3lp  7672  rankxpsuc  7806  sdomsdomcardi  7858  cardmin2  7885  pm54.43lem  7886  alephgeom  7963  alephval3  7991  pwcdadom  8096  cfsuc  8137  cflim2  8143  alephval2  8447  axunnd  8471  canthp1lem1  8527  pwxpndom2  8540  rankcf  8652  pinq  8804  adderpq  8833  mulerpq  8834  nqpr  8891  ltsopr  8909  ltapr  8922  renepnf  9132  renemnf  9133  lt0ne0d  9592  prodgt0  9855  nnne0  10032  xrltnr  10720  pnfnlt  10725  nltmnf  10726  xrltnsym  10730  nltpnft  10754  ngtmnft  10755  xsubge0  10840  xmullem2  10844  xlemul1a  10867  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  uzinf  11305  hashnemnf  11628  hashclb  11641  hasheq0  11644  hashnn0n0nn  11664  cats1un  11790  geolim  12647  geolim2  12648  georeclim  12649  geoisumr  12655  bitsfzolem  12946  bitsfzo  12947  bitsinv1lem  12953  sadcp1  12967  saddisjlem  12976  smu01lem  12997  3prm  13096  pcgcd1  13250  pc2dvds  13252  pcmpt  13261  prmreclem5  13288  vdwap0  13344  setcepi  14243  oduclatb  14571  cntzrcl  15126  odhash3  15210  gsumzaddlem  15526  gsumzsplit  15529  dprdcntz2  15596  mplcoe1  16528  mplcoe2  16530  mplrcl  16550  psrbagsn  16555  strov2rcl  16631  xrsdsreclblem  16744  istps  17001  haust1  17416  hauspwdom  17564  kqcldsat  17765  csdfil  17926  tsmssplit  18181  dscopn  18621  htpycc  19005  pco1  19040  pcohtpylem  19044  pcopt  19047  pcopt2  19048  pcoass  19049  pcorevlem  19051  itg11  19583  bddmulibl  19730  lhop1  19898  deg1nn0clb  20013  plypf1  20131  vieta1lem2  20228  logdmn0  20531  logcnlem3  20535  fsumharmonic  20850  sqff1o  20965  perfectlem1  21013  bposlem5  21072  lgsval2lem  21090  ostth  21333  umgrafi  21357  ex-res  21749  gxnval  21848  norm1exi  22752  dmadjrnb  23409  strlem1  23753  largei  23770  ifeqeqx  24001  ubico  24138  dya2iocuni  24633  ballotlem4  24756  subfacp1lem1  24865  opelco3  25403  wsuclem  25576  sltval2  25611  sltintdifex  25618  sltres  25619  dfrdg4  25795  axlowdimlem13  25893  axlowdimlem16  25896  axlowdim1  25898  axlowdim  25900  linedegen  26077  rankeq1o  26112  hfninf  26127  ordcmp  26197  mblfinlem1  26243  diophin  26831  fiphp3d  26880  expdioph  27094  wepwsolem  27116  kelac1  27138  dsmmbas2  27180  dsmmfi  27181  uvcff  27217  islindf4  27285  pmtrfrn  27377  psgnunilem5  27394  stoweidlem34  27759  elpadd0  30606
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