Theorem mtbiri 327

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 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 199	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 207

This theorem is referenced by:  psstr  4059  nel02  4291  n0i  4292  sbcel12  4363  sbcel2  4370  sbcbr123  5152  sbcbr  5153  axnul  5250  intex  5289  intnex  5290  iin0  5307  notzfaus  5308  nfcvb  5321  eunex  5335  opelopabsb  5478  brabv  5514  epelg  5525  0nelelxp  5659  elimasni  6050  onxpdisj  6444  ndmfvrcl  6867  canth  7312  oprssdm  7539  ndmovrcl  7544  omelon2  7821  poxp2  8085  xpord2indlem  8089  poxp3  8092  undefnel2  8219  tfr2b  8327  tz7.44-3  8339  nlim2  8417  ord1eln01  8423  ord2eln012  8424  1ellim  8425  2ellim  8426  eceqoveq  8759  2dom  8967  omxpenlem  9006  domunsn  9055  disjen  9062  infensuc  9083  ordfin  9140  0sdom1dom  9146  1sdom2dom  9154  infn0  9202  elfi2  9317  en3lp  9523  preleqALT  9526  rankxpsuc  9794  updjudhcoinrg  9845  sdomsdomcardi  9883  cardmin2  9911  pm54.43lem  9912  pr2ne  9915  alephgeom  9992  alephval3  10020  cfsuc  10167  cflim2  10173  alephval2  10483  axunnd  10507  canthp1lem1  10563  pwxpndom2  10576  rankcf  10688  pinq  10838  adderpq  10867  mulerpq  10868  nqpr  10925  ltsopr  10943  ltapr  10956  renepnf  11180  renemnf  11181  lt0ne0d  11702  prodgt0  11988  nnne0ALT  12183  nn0nepnf  12482  xrltnr  13033  pnfnlt  13042  nltmnf  13043  xrltnsym  13051  nltpnft  13079  ngtmnft  13081  xsubge0  13176  xmullem2  13180  xlemul1a  13203  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  fzpreddisj  13489  fzm1  13523  uzinf  13888  hashnemnf  14267  hashclb  14281  hasheq0  14286  hashnn0n0nn  14314  prprrab  14396  tpf1ofv1  14420  tpf1ofv2  14421  lsw0  14488  cats1un  14644  geolim  15793  geolim2  15794  georeclim  15795  geoisumr  15801  m1exp1  16303  bitsfzolem  16361  bitsfzo  16362  bitsinv1lem  16368  sadcp1  16382  saddisjlem  16391  smu01lem  16412  3prm  16621  pcgcd1  16805  pc2dvds  16807  pcmpt  16820  prmreclem5  16848  vdwap0  16904  prmo1  16965  fvprif  17482  setcepi  18012  oduclatb  18430  chnccats1  18548  chnccat  18549  smndex1n0mnd  18837  cntzrcl  19256  pmtrfrn  19387  pmtrprfval  19416  pmtrprfvalrn  19417  psgnunilem5  19423  odhash3  19505  gsumzaddlem  19850  gsumzsplit  19856  dprdcntz2  19969  trivnsimpgd  20028  0ringnnzr  20458  xrsdsreclblem  21367  dsmmfi  21693  islindf4  21793  mplcoe1  21992  mplcoe5  21995  psrbagsn  22018  pmatcollpw3fi1lem1  22730  istps  22878  haust1  23296  hauspwdom  23445  kqcldsat  23677  csdfil  23838  tsmssplit  24096  dscopn  24517  htpycc  24935  pco1  24971  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  itg11  25648  bddmulibl  25796  lhop1  25975  deg1nn0clb  26051  plypf1  26173  vieta1lem2  26275  logdmn0  26605  logcnlem3  26609  fsumharmonic  26978  sqff1o  27148  perfectlem1  27196  bposlem5  27255  lgsval2lem  27274  addsqrexnreu  27409  addsqnreup  27410  ostth  27606  ltsval2  27624  ltsintdifex  27629  ltsres  27630  nolt02o  27663  nogt01o  27664  bday1  27810  lrold  27893  lrrecpo  27937  mulsval  28105  legso  28671  axlowdimlem13  29027  axlowdimlem16  29030  axlowdim1  29032  axlowdim  29034  upgrfi  29164  lfgrnloop  29198  umgredgnlp  29220  wlkp1lem3  29747  rusgrnumwwlkl1  30044  clwwlk  30058  clwwlkn0  30103  clwwlknon1sn  30175  trlsegvdeg  30302  konigsberg  30332  ex-res  30516  norm1exi  31325  dmadjrnb  31981  strlem1  32325  largei  32342  ifeqeqx  32617  ubico  32855  expgt0b  32897  0ringirng  33846  rtelextdg2lem  33883  2sqr3minply  33937  dya2iocuni  34440  eulerpartlemgh  34535  ballotlem4  34656  plymulx0  34704  signswch  34718  signstfvneq0  34729  signlem0  34744  xoromon  35245  fineqvomonb  35275  noinfepfnregs  35288  subfacp1lem1  35373  fmlaomn0  35584  gonan0  35586  goaln0  35587  fmla0disjsuc  35592  ex-sategoelelomsuc  35620  ex-sategoelel12  35621  prv1n  35625  bcneg1  35930  opelco3  35969  wsuclem  36017  dfrdg4  36145  linedegen  36337  rankeq1o  36365  hfninf  36380  ordcmp  36641  curryset  37147  currysetlem3  37150  bj-projval  37197  bj-inftyexpitaudisj  37406  bj-inftyexpidisj  37411  irrdiff  37527  relowlpssretop  37565  finxpreclem2  37591  finxpreclem3  37594  finxpreclem5  37596  nlpineqsn  37609  poimirlem18  37835  poimirlem19  37836  poimirlem20  37837  mblfinlem1  37854  elpadd0  40065  pssn0  42479  oexpreposd  42573  diophin  43010  fiphp3d  43057  expdioph  43261  wepwsolem  43280  kelac1  43301  onov0suclim  43512  tfsconcatb0  43582  ensucne0  43766  relintabex  43818  brnonrel  43826  relexp01min  43950  iooinlbub  45743  stoweidlem34  46274  fourierdlem60  46406  fourierdlem61  46407  afv20defat  47474  minusmodnep2tmod  47595  spr0nelg  47718  sprsymrelfvlem  47732  fmtnoinf  47778  fmtno4prmfac193  47815  fmtno4prm  47817  31prm  47839  lighneallem3  47849  lighneallem4  47852  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  dig2nn1st  48847  itcoval1  48905  line2ylem  48993  ipolub00  49234  fucofvalne  49566