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

Theorem mtbiri 317
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 219 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 190 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  psstr  3709  n0i  3918  sbcel12  3981  sbcel2  3987  sbcbr123  4704  sbcbr  4705  axnul  4786  intex  4818  intnex  4819  iin0  4837  nfcvb  4896  opelopabsb  4983  0nelelxp  5143  elimasni  5490  0ellim  5785  onxpdisj  5845  ndmfvrcl  6217  canth  6605  fvmptopab  6694  brabv  6696  oprssdm  6812  ndmovrcl  6817  omelon2  7074  undefnel2  7400  tfr2b  7489  tz7.44-3  7501  omeulem1  7659  eceqoveq  7850  2dom  8026  omxpenlem  8058  domunsn  8107  disjen  8114  infensuc  8135  snnen2o  8146  elfi2  8317  en3lp  8510  preleq  8511  rankxpsuc  8742  sdomsdomcardi  8794  cardmin2  8821  pm54.43lem  8822  alephgeom  8902  alephval3  8930  pwcdadom  9035  cfsuc  9076  cflim2  9082  alephval2  9391  axunnd  9415  canthp1lem1  9471  pwxpndom2  9484  rankcf  9596  pinq  9746  adderpq  9775  mulerpq  9776  nqpr  9833  ltsopr  9851  ltapr  9864  renepnf  10084  renemnf  10085  lt0ne0d  10590  prodgt0  10865  nnne0  11050  nn0nepnf  11368  xrltnr  11950  pnfnlt  11959  nltmnf  11960  xrltnsym  11967  nltpnft  11992  ngtmnft  11994  xsubge0  12088  xmullem2  12092  xlemul1a  12115  xrsupsslem  12134  xrinfmsslem  12135  xrub  12139  fzpreddisj  12387  fzm1  12416  uzinf  12759  hashnemnf  13127  hashclb  13144  hasheq0  13149  hashnn0n0nn  13175  prprrab  13250  lsw0  13347  cats1un  13469  geolim  14595  geolim2  14596  georeclim  14597  geoisumr  14603  m1exp1  15087  bitsfzolem  15150  bitsfzo  15151  bitsinv1lem  15157  sadcp1  15171  saddisjlem  15180  smu01lem  15201  3prm  15400  pcgcd1  15575  pc2dvds  15577  pcmpt  15590  prmreclem5  15618  vdwap0  15674  setcepi  16732  oduclatb  17138  cntzrcl  17754  pmtrfrn  17872  pmtrprfval  17901  pmtrprfvalrn  17902  psgnunilem5  17908  odhash3  17985  gsumzaddlem  18315  gsumzsplit  18321  dprdcntz2  18431  0ringnnzr  19263  mplcoe1  19459  mplcoe5  19462  psrbagsn  19489  xrsdsreclblem  19786  dsmmbas2  20075  dsmmfi  20076  islindf4  20171  pmatcollpw3fi1lem1  20585  istps  20732  haust1  21150  hauspwdom  21298  kqcldsat  21530  csdfil  21692  tsmssplit  21949  dscopn  22372  htpycc  22773  pco1  22809  pcohtpylem  22813  pcopt  22816  pcopt2  22817  pcoass  22818  pcorevlem  22820  itg11  23452  bddmulibl  23599  lhop1  23771  deg1nn0clb  23844  plypf1  23962  vieta1lem2  24060  logdmn0  24380  logcnlem3  24384  fsumharmonic  24732  sqff1o  24902  perfectlem1  24948  bposlem5  25007  lgsval2lem  25026  ostth  25322  legso  25488  axlowdimlem13  25828  axlowdimlem16  25831  axlowdim1  25833  axlowdim  25835  upgrfi  25980  lfgrnloop  26014  umgredgnlp  26036  uvtxa01vtx  26292  wlkp1lem3  26566  rusgrnumwwlkl1  26857  clwwlks  26873  trlsegvdeg  27080  konigsberg  27112  ex-res  27282  norm1exi  28091  dmadjrnb  28749  strlem1  29093  largei  29110  ifeqeqx  29345  ubico  29522  dya2iocuni  30330  eulerpartlemgh  30425  ballotlem4  30545  plymulx0  30609  signswch  30623  signstfvneq0  30634  signlem0  30649  subfacp1lem1  31146  bcneg1  31608  opelco3  31662  wsuclem  31757  wsuclemOLD  31758  sltval2  31793  sltintdifex  31798  sltres  31799  nolt02o  31829  dfrdg4  32042  linedegen  32234  rankeq1o  32262  hfninf  32277  ordcmp  32430  bj-projval  32968  bj-inftyexpidisj  33077  relowlpssretop  33192  finxpreclem2  33207  finxpreclem3  33210  finxpreclem5  33212  poimirlem18  33407  poimirlem19  33408  poimirlem20  33409  mblfinlem1  33426  elpadd0  34921  diophin  37162  fiphp3d  37209  expdioph  37416  wepwsolem  37438  kelac1  37459  relintabex  37713  brnonrel  37721  relexp01min  37831  iooinlbub  39532  stoweidlem34  40020  fourierdlem60  40152  fourierdlem61  40153  fmtnoinf  41219  fmtno4prmfac193  41256  fmtno4prm  41258  31prm  41283  lighneallem3  41295  lighneallem4  41298  nnsum4primeseven  41459  nnsum4primesevenALTV  41460  spr0nelg  41497  sprsymrelfvlem  41511  dig2nn1st  42170
  Copyright terms: Public domain W3C validator