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

Theorem mtbiri 328
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 230 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 200 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  psstr  4080  nel02  4297  n0i  4298  sbcel12  4359  sbcel2  4366  sbcbr123  5112  sbcbr  5113  axnul  5201  intex  5232  intnex  5233  iin0  5253  notzfaus  5254  nfcvb  5269  eunex  5282  opelopabsb  5409  brabv  5445  epelg  5460  0nelelxp  5584  elimasni  5950  0ellim  6247  onxpdisj  6304  ndmfvrcl  6695  canth  7100  fvmptopab  7198  oprssdm  7318  ndmovrcl  7323  omelon2  7580  undefnel2  7934  tfr2b  8023  tz7.44-3  8035  eceqoveq  8392  2dom  8571  omxpenlem  8607  domunsn  8656  disjen  8663  infensuc  8684  snnen2o  8696  elfi2  8867  en3lp  9066  preleqALT  9069  rankxpsuc  9300  updjudhcoinrg  9351  sdomsdomcardi  9389  cardmin2  9416  pm54.43lem  9417  alephgeom  9497  alephval3  9525  cfsuc  9668  cflim2  9674  alephval2  9983  axunnd  10007  canthp1lem1  10063  pwxpndom2  10076  rankcf  10188  pinq  10338  adderpq  10367  mulerpq  10368  nqpr  10425  ltsopr  10443  ltapr  10456  renepnf  10678  renemnf  10679  lt0ne0d  11194  prodgt0  11476  nnne0ALT  11664  nn0nepnf  11964  xrltnr  12504  pnfnlt  12513  nltmnf  12514  xrltnsym  12520  nltpnft  12547  ngtmnft  12549  xsubge0  12644  xmullem2  12648  xlemul1a  12671  xrsupsslem  12690  xrinfmsslem  12691  xrub  12695  fzpreddisj  12946  fzm1  12977  uzinf  13323  hashnemnf  13694  hashclb  13709  hasheq0  13714  hashnn0n0nn  13742  prprrab  13821  lsw0  13907  cats1un  14073  geolim  15216  geolim2  15217  georeclim  15218  geoisumr  15224  m1exp1  15717  bitsfzolem  15773  bitsfzo  15774  bitsinv1lem  15780  sadcp1  15794  saddisjlem  15803  smu01lem  15824  3prm  16028  pcgcd1  16203  pc2dvds  16205  pcmpt  16218  prmreclem5  16246  vdwap0  16302  prmo1  16363  fvprif  16824  setcepi  17338  oduclatb  17744  cntzrcl  18397  pmtrfrn  18517  pmtrprfval  18546  pmtrprfvalrn  18547  psgnunilem5  18553  odhash3  18632  gsumzaddlem  18972  gsumzsplit  18978  dprdcntz2  19091  trivnsimpgd  19150  0ringnnzr  19972  mplcoe1  20176  mplcoe5  20179  psrbagsn  20205  xrsdsreclblem  20521  dsmmfi  20812  islindf4  20912  pmatcollpw3fi1lem1  21324  istps  21472  haust1  21890  hauspwdom  22039  kqcldsat  22271  csdfil  22432  tsmssplit  22689  dscopn  23112  htpycc  23513  pco1  23548  pcohtpylem  23552  pcopt  23555  pcopt2  23556  pcoass  23557  pcorevlem  23559  itg11  24221  bddmulibl  24368  lhop1  24540  deg1nn0clb  24613  plypf1  24731  vieta1lem2  24829  logdmn0  25150  logcnlem3  25154  fsumharmonic  25517  sqff1o  25687  perfectlem1  25733  bposlem5  25792  lgsval2lem  25811  addsqrexnreu  25946  addsqnreup  25947  ostth  26143  legso  26313  axlowdimlem13  26668  axlowdimlem16  26671  axlowdim1  26673  axlowdim  26675  upgrfi  26804  lfgrnloop  26838  umgredgnlp  26860  wlkp1lem3  27385  rusgrnumwwlkl1  27675  clwwlk  27689  clwwlkn0  27734  clwwlknon1sn  27807  trlsegvdeg  27934  konigsberg  27964  ex-res  28148  norm1exi  28955  dmadjrnb  29611  strlem1  29955  largei  29972  ifeqeqx  30225  ubico  30425  dya2iocuni  31441  eulerpartlemgh  31536  ballotlem4  31656  plymulx0  31717  signswch  31731  signstfvneq0  31742  signlem0  31757  subfacp1lem1  32324  fmlaomn0  32535  gonan0  32537  goaln0  32538  fmla0disjsuc  32543  ex-sategoelelomsuc  32571  ex-sategoelel12  32572  prv1n  32576  bcneg1  32866  opelco3  32916  wsuclem  33010  sltval2  33061  sltintdifex  33066  sltres  33067  nolt02o  33097  dfrdg4  33310  linedegen  33502  rankeq1o  33530  hfninf  33545  ordcmp  33693  curryset  34155  currysetlem3  34158  bj-projval  34206  bj-inftyexpitaudisj  34380  bj-inftyexpidisj  34385  relowlpssretop  34528  finxpreclem2  34554  finxpreclem3  34557  finxpreclem5  34559  nlpineqsn  34572  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  mblfinlem1  34811  elpadd0  36827  pssn0  38993  oexpreposd  39059  diophin  39249  fiphp3d  39296  expdioph  39500  wepwsolem  39522  kelac1  39543  ensucne0  39775  relintabex  39821  brnonrel  39829  relexp01min  39938  iooinlbub  41656  stoweidlem34  42200  fourierdlem60  42332  fourierdlem61  42333  afv20defat  43312  spr0nelg  43485  sprsymrelfvlem  43499  fmtnoinf  43545  fmtno4prmfac193  43582  fmtno4prm  43584  31prm  43607  lighneallem3  43619  lighneallem4  43622  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  smndex1n0mnd  43982  dig2nn1st  44563  line2ylem  44636
  Copyright terms: Public domain W3C validator