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

Theorem mtbiri 318
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 220 . 2 (𝜑 → (𝜓𝜒))
41, 3mtoi 190 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197
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 198
This theorem is referenced by:  psstr  3920  n0i  4132  sbcel12  4191  sbcel2  4197  sbcbr123  4909  sbcbr  4910  axnul  4995  intex  5025  intnex  5026  iin0  5044  nfcvb  5059  opelopabsb  5193  0nelelxp  5358  elimasni  5716  0ellim  6013  onxpdisj  6070  ndmfvrcl  6449  canth  6842  fvmptopab  6937  brabv  6939  oprssdm  7055  ndmovrcl  7060  omelon2  7317  undefnel2  7648  tfr2b  7738  tz7.44-3  7750  omeulem1  7909  eceqoveq  8098  2dom  8275  omxpenlem  8310  domunsn  8359  disjen  8366  infensuc  8387  snnen2o  8398  elfi2  8569  en3lp  8766  preleqALT  8769  preleqOLD  8771  rankxpsuc  9002  updjudhcoinrg  9052  sdomsdomcardi  9090  cardmin2  9117  pm54.43lem  9118  alephgeom  9198  alephval3  9226  pwcdadom  9333  cfsuc  9374  cflim2  9380  alephval2  9689  axunnd  9713  canthp1lem1  9769  pwxpndom2  9782  rankcf  9894  pinq  10044  adderpq  10073  mulerpq  10074  nqpr  10131  ltsopr  10149  ltapr  10162  renepnf  10382  renemnf  10383  lt0ne0d  10888  prodgt0  11163  nnne0  11351  nn0nepnf  11657  xrltnr  12189  pnfnlt  12198  nltmnf  12199  xrltnsym  12206  nltpnft  12233  ngtmnft  12235  xsubge0  12329  xmullem2  12333  xlemul1a  12356  xrsupsslem  12375  xrinfmsslem  12376  xrub  12380  fzpreddisj  12633  fzm1  12663  uzinf  13008  hashnemnf  13372  hashclb  13387  hasheq0  13392  hashnn0n0nn  13418  prprrab  13492  lsw0  13584  cats1un  13719  geolim  14843  geolim2  14844  georeclim  14845  geoisumr  14851  m1exp1  15333  bitsfzolem  15395  bitsfzo  15396  bitsinv1lem  15402  sadcp1  15416  saddisjlem  15425  smu01lem  15446  3prm  15644  pcgcd1  15818  pc2dvds  15820  pcmpt  15833  prmreclem5  15861  vdwap0  15917  setcepi  16962  oduclatb  17369  cntzrcl  17981  pmtrfrn  18099  pmtrprfval  18128  pmtrprfvalrn  18129  psgnunilem5  18135  odhash3  18212  gsumzaddlem  18542  gsumzsplit  18548  dprdcntz2  18659  0ringnnzr  19498  mplcoe1  19694  mplcoe5  19697  psrbagsn  19723  xrsdsreclblem  20020  dsmmbas2  20312  dsmmfi  20313  islindf4  20408  pmatcollpw3fi1lem1  20825  istps  20973  haust1  21391  hauspwdom  21539  kqcldsat  21771  csdfil  21932  tsmssplit  22189  dscopn  22612  htpycc  23013  pco1  23048  pcohtpylem  23052  pcopt  23055  pcopt2  23056  pcoass  23057  pcorevlem  23059  itg11  23695  bddmulibl  23842  lhop1  24014  deg1nn0clb  24087  plypf1  24205  vieta1lem2  24303  logdmn0  24623  logcnlem3  24627  fsumharmonic  24975  sqff1o  25145  perfectlem1  25191  bposlem5  25250  lgsval2lem  25269  ostth  25565  legso  25731  axlowdimlem13  26071  axlowdimlem16  26074  axlowdim1  26076  axlowdim  26078  upgrfi  26223  lfgrnloop  26257  umgredgnlp  26280  wlkp1lem3  26823  rusgrnumwwlkl1  27133  clwwlk  27149  clwwlkn0  27198  clwwlknon1sn  27291  trlsegvdeg  27423  konigsberg  27453  ex-res  27652  norm1exi  28458  dmadjrnb  29116  strlem1  29460  largei  29477  ifeqeqx  29709  ubico  29887  dya2iocuni  30693  eulerpartlemgh  30788  ballotlem4  30908  plymulx0  30972  signswch  30986  signstfvneq0  30997  signlem0  31012  subfacp1lem1  31506  bcneg1  31966  opelco3  32020  wsuclem  32113  sltval2  32152  sltintdifex  32157  sltres  32158  nolt02o  32188  dfrdg4  32401  linedegen  32593  rankeq1o  32621  hfninf  32636  ordcmp  32785  bj-projval  33313  bj-inftyexpidisj  33433  relowlpssretop  33547  finxpreclem2  33562  finxpreclem3  33565  finxpreclem5  33567  poimirlem18  33759  poimirlem19  33760  poimirlem20  33761  mblfinlem1  33778  nel02  34431  elpadd0  35608  pssn0  37769  diophin  37856  fiphp3d  37903  expdioph  38109  wepwsolem  38131  kelac1  38152  relintabex  38405  brnonrel  38413  relexp01min  38523  iooinlbub  40225  stoweidlem34  40748  fourierdlem60  40880  fourierdlem61  40881  afv20defat  41839  fmtnoinf  42041  fmtno4prmfac193  42078  fmtno4prm  42080  31prm  42105  lighneallem3  42117  lighneallem4  42120  nnsum4primeseven  42281  nnsum4primesevenALTV  42282  spr0nelg  42312  sprsymrelfvlem  42326  dig2nn1st  42985
  Copyright terms: Public domain W3C validator