Theorem mtbiri 326

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

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 ⊢ ¬ 𝜒
2		mtbiri.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 228	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 198	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  psstr  4100  nel02  4328  n0i  4329  sbcel12  4404  sbcel2  4411  sbcbr123  5195  sbcbr  5196  axnul  5298  intex  5330  intnex  5331  iin0  5353  notzfaus  5354  nfcvb  5367  eunex  5381  opelopabsb  5523  brabv  5562  epelg  5574  0nelelxp  5704  elimasni  6079  0ellim  6416  onxpdisj  6479  ndmfvrcl  6914  canth  7346  fvmptopabOLD  7448  oprssdm  7571  ndmovrcl  7576  omelon2  7851  poxp2  8111  xpord2indlem  8115  poxp3  8118  undefnel2  8244  tfr2b  8378  tz7.44-3  8390  nlim2  8472  ord1eln01  8478  ord2eln012  8479  1ellim  8480  2ellim  8481  eceqoveq  8799  2dom  9013  omxpenlem  9056  domunsn  9110  disjen  9117  infensuc  9138  snnen2oOLD  9210  0sdom1dom  9221  1sdom2dom  9230  infn0  9290  elfi2  9391  en3lp  9591  preleqALT  9594  rankxpsuc  9859  updjudhcoinrg  9910  sdomsdomcardi  9948  cardmin2  9976  pm54.43lem  9977  pr2ne  9981  alephgeom  10059  alephval3  10087  cfsuc  10234  cflim2  10240  alephval2  10549  axunnd  10573  canthp1lem1  10629  pwxpndom2  10642  rankcf  10754  pinq  10904  adderpq  10933  mulerpq  10934  nqpr  10991  ltsopr  11009  ltapr  11022  renepnf  11244  renemnf  11245  lt0ne0d  11761  prodgt0  12043  nnne0ALT  12232  nn0nepnf  12534  xrltnr  13081  pnfnlt  13090  nltmnf  13091  xrltnsym  13098  nltpnft  13125  ngtmnft  13127  xsubge0  13222  xmullem2  13226  xlemul1a  13249  xrsupsslem  13268  xrinfmsslem  13269  xrub  13273  fzpreddisj  13532  fzm1  13563  uzinf  13912  hashnemnf  14286  hashclb  14300  hasheq0  14305  hashnn0n0nn  14333  prprrab  14416  lsw0  14497  cats1un  14653  geolim  15798  geolim2  15799  georeclim  15800  geoisumr  15806  m1exp1  16301  bitsfzolem  16357  bitsfzo  16358  bitsinv1lem  16364  sadcp1  16378  saddisjlem  16387  smu01lem  16408  3prm  16613  pcgcd1  16792  pc2dvds  16794  pcmpt  16807  prmreclem5  16835  vdwap0  16891  prmo1  16952  fvprif  17489  setcepi  18020  oduclatb  18442  smndex1n0mnd  18768  cntzrcl  19157  pmtrfrn  19290  pmtrprfval  19319  pmtrprfvalrn  19320  psgnunilem5  19326  odhash3  19408  gsumzaddlem  19748  gsumzsplit  19754  dprdcntz2  19867  trivnsimpgd  19926  0ringnnzr  20252  xrsdsreclblem  20925  dsmmfi  21226  islindf4  21326  mplcoe1  21520  mplcoe5  21523  psrbagsn  21553  pmatcollpw3fi1lem1  22217  istps  22365  haust1  22785  hauspwdom  22934  kqcldsat  23166  csdfil  23327  tsmssplit  23585  dscopn  24011  htpycc  24425  pco1  24460  pcohtpylem  24464  pcopt  24467  pcopt2  24468  pcoass  24469  pcorevlem  24471  itg11  25137  bddmulibl  25285  lhop1  25460  deg1nn0clb  25537  plypf1  25655  vieta1lem2  25753  logdmn0  26077  logcnlem3  26081  fsumharmonic  26443  sqff1o  26613  perfectlem1  26659  bposlem5  26718  lgsval2lem  26737  addsqrexnreu  26872  addsqnreup  26873  ostth  27069  sltval2  27086  sltintdifex  27091  sltres  27092  nolt02o  27125  nogt01o  27126  bday1s  27258  lrold  27314  lrrecpo  27341  mulsval  27479  legso  27715  axlowdimlem13  28077  axlowdimlem16  28080  axlowdim1  28082  axlowdim  28084  upgrfi  28216  lfgrnloop  28250  umgredgnlp  28272  wlkp1lem3  28797  rusgrnumwwlkl1  29087  clwwlk  29101  clwwlkn0  29146  clwwlknon1sn  29218  trlsegvdeg  29345  konigsberg  29375  ex-res  29559  norm1exi  30366  dmadjrnb  31022  strlem1  31366  largei  31383  ifeqeqx  31639  ubico  31857  0ringirng  32589  dya2iocuni  33111  eulerpartlemgh  33206  ballotlem4  33326  plymulx0  33387  signswch  33401  signstfvneq0  33412  signlem0  33427  subfacp1lem1  33999  fmlaomn0  34210  gonan0  34212  goaln0  34213  fmla0disjsuc  34218  ex-sategoelelomsuc  34246  ex-sategoelel12  34247  prv1n  34251  bcneg1  34534  opelco3  34574  wsuclem  34625  dfrdg4  34751  linedegen  34943  rankeq1o  34971  hfninf  34986  ordcmp  35134  curryset  35629  currysetlem3  35632  bj-projval  35679  bj-inftyexpitaudisj  35888  bj-inftyexpidisj  35893  irrdiff  36009  relowlpssretop  36047  finxpreclem2  36073  finxpreclem3  36076  finxpreclem5  36078  nlpineqsn  36091  poimirlem18  36308  poimirlem19  36309  poimirlem20  36310  mblfinlem1  36327  elpadd0  38483  pssn0  40858  oexpreposd  40991  diophin  41279  fiphp3d  41326  expdioph  41531  wepwsolem  41553  kelac1  41574  onov0suclim  41793  tfsconcatb0  41863  ensucne0  42049  relintabex  42101  brnonrel  42109  relexp01min  42233  iooinlbub  43985  stoweidlem34  44521  fourierdlem60  44653  fourierdlem61  44654  tworepnotupword  45371  afv20defat  45710  spr0nelg  45914  sprsymrelfvlem  45928  fmtnoinf  45974  fmtno4prmfac193  46011  fmtno4prm  46013  31prm  46035  lighneallem3  46045  lighneallem4  46048  nnsum4primeseven  46238  nnsum4primesevenALTV  46239  dig2nn1st  46937  itcoval1  46995  line2ylem  47083  ipolub00  47264