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

Theorem mtbiri 296
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 200 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtoi 172 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  psstr  3453  n0i  3635  axnul  4339  intex  4358  intnex  4359  iin0  4375  nfcvb  4396  opelopabsb  4467  0ellim  4645  omelon2  4859  0nelelxp  4909  onxpdisj  4959  elimasni  5233  ndmfvrcl  5758  brabv  6122  oprssdm  6230  ndmovrcl  6235  canth  6541  undefnel2  6549  tfr2b  6659  tz7.44-3  6668  omeulem1  6827  eceqoveq  7011  2dom  7181  omxpenlem  7211  domunsn  7259  disjen  7266  infensuc  7287  elfi2  7421  sucprcreg  7569  preleq  7574  en3lp  7674  rankxpsuc  7808  sdomsdomcardi  7860  cardmin2  7887  pm54.43lem  7888  alephgeom  7965  alephval3  7993  pwcdadom  8098  cfsuc  8139  cflim2  8145  alephval2  8449  axunnd  8473  canthp1lem1  8529  pwxpndom2  8542  rankcf  8654  pinq  8806  adderpq  8835  mulerpq  8836  nqpr  8893  ltsopr  8911  ltapr  8924  renepnf  9134  renemnf  9135  lt0ne0d  9594  prodgt0  9857  nnne0  10034  xrltnr  10722  pnfnlt  10727  nltmnf  10728  xrltnsym  10732  nltpnft  10756  ngtmnft  10757  xsubge0  10842  xmullem2  10846  xlemul1a  10869  xrsupsslem  10887  xrinfmsslem  10888  xrub  10892  uzinf  11307  hashnemnf  11630  hashclb  11643  hasheq0  11646  hashnn0n0nn  11666  cats1un  11792  geolim  12649  geolim2  12650  georeclim  12651  geoisumr  12657  bitsfzolem  12948  bitsfzo  12949  bitsinv1lem  12955  sadcp1  12969  saddisjlem  12978  smu01lem  12999  3prm  13098  pcgcd1  13252  pc2dvds  13254  pcmpt  13263  prmreclem5  13290  vdwap0  13346  setcepi  14245  oduclatb  14573  cntzrcl  15128  odhash3  15212  gsumzaddlem  15528  gsumzsplit  15531  dprdcntz2  15598  mplcoe1  16530  mplcoe2  16532  mplrcl  16552  psrbagsn  16557  strov2rcl  16633  xrsdsreclblem  16746  istps  17003  haust1  17418  hauspwdom  17566  kqcldsat  17767  csdfil  17928  tsmssplit  18183  dscopn  18623  htpycc  19007  pco1  19042  pcohtpylem  19046  pcopt  19049  pcopt2  19050  pcoass  19051  pcorevlem  19053  itg11  19585  bddmulibl  19732  lhop1  19900  deg1nn0clb  20015  plypf1  20133  vieta1lem2  20230  logdmn0  20533  logcnlem3  20537  fsumharmonic  20852  sqff1o  20967  perfectlem1  21015  bposlem5  21074  lgsval2lem  21092  ostth  21335  umgrafi  21359  ex-res  21751  gxnval  21850  norm1exi  22754  dmadjrnb  23411  strlem1  23755  largei  23772  ifeqeqx  24003  ubico  24140  dya2iocuni  24635  ballotlem4  24758  subfacp1lem1  24867  opelco3  25405  wsuclem  25578  sltval2  25613  sltintdifex  25620  sltres  25621  dfrdg4  25797  axlowdimlem13  25895  axlowdimlem16  25898  axlowdim1  25900  axlowdim  25902  linedegen  26079  rankeq1o  26114  hfninf  26129  ordcmp  26199  mblfinlem1  26245  diophin  26833  fiphp3d  26882  expdioph  27096  wepwsolem  27118  kelac1  27140  dsmmbas2  27182  dsmmfi  27183  uvcff  27219  islindf4  27287  pmtrfrn  27379  psgnunilem5  27396  stoweidlem34  27761  elpadd0  30668
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 179
  Copyright terms: Public domain W3C validator