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

Theorem mtbiri 315
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 217 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 188 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  psstr  3668  n0i  3874  sbcel12  3930  sbcel2  3936  sbcbr123  4626  sbcbr  4627  axnul  4706  axnulOLD  4707  intex  4738  intnex  4739  iin0  4756  nfcvb  4815  opelopabsb  4896  0nelelxp  5055  elimasni  5394  0ellim  5686  onxpdisj  5746  ndmfvrcl  6110  canth  6482  brabv  6571  oprssdm  6686  ndmovrcl  6691  omelon2  6942  undefnel2  7263  tfr2b  7352  tz7.44-3  7364  omeulem1  7522  eceqoveq  7713  2dom  7888  omxpenlem  7919  domunsn  7968  disjen  7975  infensuc  7996  snnen2o  8007  elfi2  8176  en3lp  8369  preleq  8370  rankxpsuc  8601  sdomsdomcardi  8653  cardmin2  8680  pm54.43lem  8681  alephgeom  8761  alephval3  8789  pwcdadom  8894  cfsuc  8935  cflim2  8941  alephval2  9246  axunnd  9270  canthp1lem1  9326  pwxpndom2  9339  rankcf  9451  pinq  9601  adderpq  9630  mulerpq  9631  nqpr  9688  ltsopr  9706  ltapr  9719  renepnf  9939  renemnf  9940  lt0ne0d  10438  prodgt0  10713  nnne0  10896  xrltnr  11786  pnfnlt  11795  nltmnf  11796  xrltnsym  11801  nltpnft  11826  ngtmnft  11827  xsubge0  11916  xmullem2  11920  xlemul1a  11943  xrsupsslem  11961  xrinfmsslem  11962  xrub  11966  fzpreddisj  12211  fzm1  12240  uzinf  12577  hashnemnf  12942  hashclb  12959  hasheq0  12963  hashnn0n0nn  12989  lsw0  13147  cats1un  13269  geolim  14382  geolim2  14383  georeclim  14384  geoisumr  14390  m1exp1  14873  bitsfzolem  14936  bitsfzo  14937  bitsinv1lem  14943  sadcp1  14957  saddisjlem  14966  smu01lem  14987  3prm  15186  pcgcd1  15361  pc2dvds  15363  pcmpt  15376  prmreclem5  15404  vdwap0  15460  setcepi  16503  oduclatb  16909  cntzrcl  17525  pmtrfrn  17643  pmtrprfval  17672  pmtrprfvalrn  17673  psgnunilem5  17679  odhash3  17756  gsumzaddlem  18086  gsumzsplit  18092  dprdcntz2  18202  0ringnnzr  19032  mplcoe1  19228  mplcoe5  19231  psrbagsn  19258  xrsdsreclblem  19553  dsmmbas2  19838  dsmmfi  19839  islindf4  19934  pmatcollpw3fi1lem1  20348  istps  20489  haust1  20904  hauspwdom  21052  kqcldsat  21284  csdfil  21446  tsmssplit  21703  dscopn  22125  htpycc  22514  pco1  22550  pcohtpylem  22554  pcopt  22557  pcopt2  22558  pcoass  22559  pcorevlem  22561  itg11  23177  bddmulibl  23324  lhop1  23494  deg1nn0clb  23567  plypf1  23685  vieta1lem2  23783  logdmn0  24099  logcnlem3  24103  fsumharmonic  24451  sqff1o  24621  perfectlem1  24667  bposlem5  24726  lgsval2lem  24745  ostth  25041  legso  25208  axlowdimlem13  25548  axlowdimlem16  25551  axlowdim1  25553  axlowdim  25555  umgrafi  25613  rusgranumwlkl1  26236  ex-res  26452  norm1exi  27293  dmadjrnb  27951  strlem1  28295  largei  28312  ifeqeqx  28547  ubico  28729  dya2iocuni  29474  eulerpartlemgh  29569  ballotlem4  29689  plymulx0  29752  signswch  29766  signstfvneq0  29777  signlem0  29792  subfacp1lem1  30217  bcneg1  30677  opelco3  30725  wsuclem  30819  wsuclemOLD  30820  sltval2  30855  sltintdifex  30862  sltres  30863  dfrdg4  31030  linedegen  31222  rankeq1o  31250  hfninf  31265  ordcmp  31418  bj-projval  31976  bj-inftyexpidisj  32073  relowlpssretop  32187  finxpreclem2  32202  finxpreclem3  32205  finxpreclem5  32207  poimirlem18  32396  poimirlem19  32397  poimirlem20  32398  mblfinlem1  32415  elpadd0  33912  diophin  36153  fiphp3d  36200  expdioph  36407  wepwsolem  36429  kelac1  36450  relintabex  36705  brnonrel  36713  relexp01min  36823  iooinlbub  38370  stoweidlem34  38727  fourierdlem60  38859  fourierdlem61  38860  fmtnoinf  39787  fmtno4prmfac193  39824  fmtno4prm  39826  31prm  39851  lighneallem3  39863  lighneallem4  39866  nnsum4primeseven  40017  nnsum4primesevenALTV  40018  prprrab  40193  nn0nepnf  40204  upgrfi  40315  lfgrnloop  40348  umgredgnlp  40375  uvtxa01vtx  40622  1wlkp1lem3  40882  rusgrnumwwlkl1  41170  clwwlks  41185  trlsegvdeg  41393  konigsberg-av  41425  dig2nn1st  42195
  Copyright terms: Public domain W3C validator