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

Theorem mtbiri 316
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)
Hypotheses
Ref Expression
mtbiri.min ¬ 𝜒
mtbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtbiri (𝜑 → ¬ 𝜓)

Proof of Theorem mtbiri
StepHypRef Expression
1 mtbiri.min . 2 ¬ 𝜒
2 mtbiri.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 218 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
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 196
This theorem is referenced by:  psstr  3673  n0i  3879  sbcel12  3935  sbcel2  3941  sbcbr123  4636  sbcbr  4637  axnul  4716  intex  4747  intnex  4748  iin0  4765  nfcvb  4824  opelopabsb  4910  0nelelxp  5069  elimasni  5411  0ellim  5704  onxpdisj  5764  ndmfvrcl  6129  canth  6508  brabv  6597  oprssdm  6713  ndmovrcl  6718  omelon2  6969  undefnel2  7290  tfr2b  7379  tz7.44-3  7391  omeulem1  7549  eceqoveq  7740  2dom  7915  omxpenlem  7946  domunsn  7995  disjen  8002  infensuc  8023  snnen2o  8034  elfi2  8203  en3lp  8396  preleq  8397  rankxpsuc  8628  sdomsdomcardi  8680  cardmin2  8707  pm54.43lem  8708  alephgeom  8788  alephval3  8816  pwcdadom  8921  cfsuc  8962  cflim2  8968  alephval2  9273  axunnd  9297  canthp1lem1  9353  pwxpndom2  9366  rankcf  9478  pinq  9628  adderpq  9657  mulerpq  9658  nqpr  9715  ltsopr  9733  ltapr  9746  renepnf  9966  renemnf  9967  lt0ne0d  10472  prodgt0  10747  nnne0  10930  nn0nepnf  11248  xrltnr  11829  pnfnlt  11838  nltmnf  11839  xrltnsym  11846  nltpnft  11871  ngtmnft  11872  xsubge0  11963  xmullem2  11967  xlemul1a  11990  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  fzpreddisj  12260  fzm1  12289  uzinf  12626  hashnemnf  12994  hashclb  13011  hasheq0  13015  hashnn0n0nn  13041  prprrab  13112  lsw0  13205  cats1un  13327  geolim  14440  geolim2  14441  georeclim  14442  geoisumr  14448  m1exp1  14931  bitsfzolem  14994  bitsfzo  14995  bitsinv1lem  15001  sadcp1  15015  saddisjlem  15024  smu01lem  15045  3prm  15244  pcgcd1  15419  pc2dvds  15421  pcmpt  15434  prmreclem5  15462  vdwap0  15518  setcepi  16561  oduclatb  16967  cntzrcl  17583  pmtrfrn  17701  pmtrprfval  17730  pmtrprfvalrn  17731  psgnunilem5  17737  odhash3  17814  gsumzaddlem  18144  gsumzsplit  18150  dprdcntz2  18260  0ringnnzr  19090  mplcoe1  19286  mplcoe5  19289  psrbagsn  19316  xrsdsreclblem  19611  dsmmbas2  19900  dsmmfi  19901  islindf4  19996  pmatcollpw3fi1lem1  20410  istps  20551  haust1  20966  hauspwdom  21114  kqcldsat  21346  csdfil  21508  tsmssplit  21765  dscopn  22188  htpycc  22587  pco1  22623  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  itg11  23264  bddmulibl  23411  lhop1  23581  deg1nn0clb  23654  plypf1  23772  vieta1lem2  23870  logdmn0  24186  logcnlem3  24190  fsumharmonic  24538  sqff1o  24708  perfectlem1  24754  bposlem5  24813  lgsval2lem  24832  ostth  25128  legso  25294  axlowdimlem13  25634  axlowdimlem16  25637  axlowdim1  25639  axlowdim  25641  upgrfi  25758  lfgrnloop  25791  umgredgnlp  25818  umgrafi  25851  rusgranumwlkl1  26474  ex-res  26690  norm1exi  27491  dmadjrnb  28149  strlem1  28493  largei  28510  ifeqeqx  28745  ubico  28927  dya2iocuni  29672  eulerpartlemgh  29767  ballotlem4  29887  plymulx0  29950  signswch  29964  signstfvneq0  29975  signlem0  29990  subfacp1lem1  30415  bcneg1  30875  opelco3  30923  wsuclem  31017  wsuclemOLD  31018  sltval2  31053  sltintdifex  31060  sltres  31061  dfrdg4  31228  linedegen  31420  rankeq1o  31448  hfninf  31463  ordcmp  31616  bj-projval  32177  bj-inftyexpidisj  32274  relowlpssretop  32388  finxpreclem2  32403  finxpreclem3  32406  finxpreclem5  32408  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  mblfinlem1  32616  elpadd0  34113  diophin  36354  fiphp3d  36401  expdioph  36608  wepwsolem  36630  kelac1  36651  relintabex  36906  brnonrel  36914  relexp01min  37024  iooinlbub  38570  stoweidlem34  38927  fourierdlem60  39059  fourierdlem61  39060  fmtnoinf  39986  fmtno4prmfac193  40023  fmtno4prm  40025  31prm  40050  lighneallem3  40062  lighneallem4  40065  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  uvtxa01vtx  40624  1wlkp1lem3  40884  rusgrnumwwlkl1  41172  clwwlks  41187  trlsegvdeg  41395  konigsberg-av  41427  dig2nn1st  42197
  Copyright terms: Public domain W3C validator