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  3460  n0i  3642  sbcel2  3683  sbcbr123  4343  axnul  4420  intex  4448  intnex  4449  iin0  4466  nfcvb  4522  opelopabsb  4599  0ellim  4781  0nelelxp  4868  onxpdisj  4920  elimasni  5196  ndmfvrcl  5715  canth  6049  brabv  6132  oprssdm  6244  ndmovrcl  6249  omelon2  6488  undefnel2  6796  tfr2b  6855  tz7.44-3  6864  omeulem1  7021  eceqoveq  7205  2dom  7382  omxpenlem  7412  domunsn  7461  disjen  7468  infensuc  7489  elfi2  7664  sucprcregOLD  7815  en3lp  7822  preleq  7823  rankxpsuc  8089  sdomsdomcardi  8141  cardmin2  8168  pm54.43lem  8169  alephgeom  8252  alephval3  8280  pwcdadom  8385  cfsuc  8426  cflim2  8432  alephval2  8736  axunnd  8760  canthp1lem1  8819  pwxpndom2  8832  rankcf  8944  pinq  9096  adderpq  9125  mulerpq  9126  nqpr  9183  ltsopr  9201  ltapr  9214  renepnf  9431  renemnf  9432  lt0ne0d  9905  prodgt0  10174  nnne0  10354  xrltnr  11101  pnfnlt  11108  nltmnf  11109  xrltnsym  11114  nltpnft  11138  ngtmnft  11139  xsubge0  11224  xmullem2  11228  xlemul1a  11251  xrsupsslem  11269  xrinfmsslem  11270  xrub  11274  fzpreddisj  11504  uzinf  11788  hashnemnf  12115  hashclb  12128  hasheq0  12131  hashnn0n0nn  12153  cats1un  12370  geolim  13330  geolim2  13331  georeclim  13332  geoisumr  13338  bitsfzolem  13630  bitsfzo  13631  bitsinv1lem  13637  sadcp1  13651  saddisjlem  13660  smu01lem  13681  3prm  13780  pcgcd1  13943  pc2dvds  13945  pcmpt  13954  prmreclem5  13981  vdwap0  14037  setcepi  14956  oduclatb  15314  cntzrcl  15845  pmtrfrn  15964  pmtrprfval  15993  pmtrprfvalrn  15994  psgnunilem5  16000  odhash3  16075  gsumzaddlem  16408  gsumzaddlemOLD  16410  gsumzsplit  16418  gsumzsplitOLD  16419  dprdcntz2  16536  mplcoe1  17544  mplcoe5  17548  mplcoe2OLD  17550  mplrcl  17571  psrbagsn  17577  strov2rcl  17692  xrsdsreclblem  17859  dsmmbas2  18162  dsmmfi  18163  islindf4  18267  istps  18541  haust1  18956  hauspwdom  19105  kqcldsat  19306  csdfil  19467  tsmssplit  19726  dscopn  20166  htpycc  20552  pco1  20587  pcohtpylem  20591  pcopt  20594  pcopt2  20595  pcoass  20596  pcorevlem  20598  itg11  21169  bddmulibl  21316  lhop1  21486  deg1nn0clb  21561  plypf1  21680  vieta1lem2  21777  logdmn0  22085  logcnlem3  22089  fsumharmonic  22405  sqff1o  22520  perfectlem1  22568  bposlem5  22627  lgsval2lem  22645  ostth  22888  axlowdimlem13  23200  axlowdimlem16  23203  axlowdim1  23205  axlowdim  23207  umgrafi  23256  ex-res  23648  gxnval  23747  norm1exi  24653  dmadjrnb  25310  strlem1  25654  largei  25671  ifeqeqx  25902  ubico  26065  dya2iocuni  26698  eulerpartlemgh  26761  ballotlem4  26881  plymulx0  26948  signswch  26962  signstfvneq0  26973  signlem0  26988  subfacp1lem1  27067  opelco3  27589  wsuclem  27762  sltval2  27797  sltintdifex  27804  sltres  27805  dfrdg4  27981  linedegen  28174  rankeq1o  28209  hfninf  28224  ordcmp  28293  mblfinlem1  28428  diophin  29111  fiphp3d  29158  expdioph  29372  wepwsolem  29394  kelac1  29416  stoweidlem34  29829  rusgranumwlkl1  30559  snnen2o  30738  0rngnnzr  30778  bj-projval  32489  bj-inftyexpidisj  32533  elpadd0  33453
  Copyright terms: Public domain W3C validator