Theorem mtbiri 330

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

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

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 210

This theorem is referenced by:  psstr  4005  nel02  4233  n0i  4234  sbcel12  4309  sbcel2  4316  sbcbr123  5093  sbcbr  5094  axnul  5183  intex  5215  intnex  5216  iin0  5238  notzfaus  5239  nfcvb  5254  eunex  5268  opelopabsb  5396  brabv  5433  epelg  5446  0nelelxp  5571  elimasni  5941  0ellim  6253  onxpdisj  6311  ndmfvrcl  6726  canth  7145  fvmptopab  7244  oprssdm  7367  ndmovrcl  7372  omelon2  7635  undefnel2  7997  tfr2b  8110  tz7.44-3  8122  eceqoveq  8482  2dom  8685  omxpenlem  8724  domunsn  8774  disjen  8781  infensuc  8802  snnen2o  8814  elfi2  9008  en3lp  9207  preleqALT  9210  rankxpsuc  9463  updjudhcoinrg  9514  sdomsdomcardi  9552  cardmin2  9580  pm54.43lem  9581  alephgeom  9661  alephval3  9689  cfsuc  9836  cflim2  9842  alephval2  10151  axunnd  10175  canthp1lem1  10231  pwxpndom2  10244  rankcf  10356  pinq  10506  adderpq  10535  mulerpq  10536  nqpr  10593  ltsopr  10611  ltapr  10624  renepnf  10846  renemnf  10847  lt0ne0d  11362  prodgt0  11644  nnne0ALT  11833  nn0nepnf  12135  xrltnr  12676  pnfnlt  12685  nltmnf  12686  xrltnsym  12692  nltpnft  12719  ngtmnft  12721  xsubge0  12816  xmullem2  12820  xlemul1a  12843  xrsupsslem  12862  xrinfmsslem  12863  xrub  12867  fzpreddisj  13126  fzm1  13157  uzinf  13503  hashnemnf  13875  hashclb  13890  hasheq0  13895  hashnn0n0nn  13923  prprrab  14004  lsw0  14085  cats1un  14251  geolim  15397  geolim2  15398  georeclim  15399  geoisumr  15405  m1exp1  15900  bitsfzolem  15956  bitsfzo  15957  bitsinv1lem  15963  sadcp1  15977  saddisjlem  15986  smu01lem  16007  3prm  16214  pcgcd1  16393  pc2dvds  16395  pcmpt  16408  prmreclem5  16436  vdwap0  16492  prmo1  16553  fvprif  17020  setcepi  17548  oduclatb  17967  smndex1n0mnd  18293  cntzrcl  18675  pmtrfrn  18804  pmtrprfval  18833  pmtrprfvalrn  18834  psgnunilem5  18840  odhash3  18919  gsumzaddlem  19260  gsumzsplit  19266  dprdcntz2  19379  trivnsimpgd  19438  0ringnnzr  20261  xrsdsreclblem  20363  dsmmfi  20654  islindf4  20754  mplcoe1  20948  mplcoe5  20951  psrbagsn  20975  pmatcollpw3fi1lem1  21637  istps  21785  haust1  22203  hauspwdom  22352  kqcldsat  22584  csdfil  22745  tsmssplit  23003  dscopn  23425  htpycc  23831  pco1  23866  pcohtpylem  23870  pcopt  23873  pcopt2  23874  pcoass  23875  pcorevlem  23877  itg11  24542  bddmulibl  24690  lhop1  24865  deg1nn0clb  24942  plypf1  25060  vieta1lem2  25158  logdmn0  25482  logcnlem3  25486  fsumharmonic  25848  sqff1o  26018  perfectlem1  26064  bposlem5  26123  lgsval2lem  26142  addsqrexnreu  26277  addsqnreup  26278  ostth  26474  legso  26644  axlowdimlem13  26999  axlowdimlem16  27002  axlowdim1  27004  axlowdim  27006  upgrfi  27136  lfgrnloop  27170  umgredgnlp  27192  wlkp1lem3  27717  rusgrnumwwlkl1  28006  clwwlk  28020  clwwlkn0  28065  clwwlknon1sn  28137  trlsegvdeg  28264  konigsberg  28294  ex-res  28478  norm1exi  29285  dmadjrnb  29941  strlem1  30285  largei  30302  ifeqeqx  30558  ubico  30770  dya2iocuni  31916  eulerpartlemgh  32011  ballotlem4  32131  plymulx0  32192  signswch  32206  signstfvneq0  32217  signlem0  32232  subfacp1lem1  32808  fmlaomn0  33019  gonan0  33021  goaln0  33022  fmla0disjsuc  33027  ex-sategoelelomsuc  33055  ex-sategoelel12  33056  prv1n  33060  bcneg1  33371  opelco3  33419  poxp2  33470  xpord2ind  33474  poxp3  33476  xpord3ind  33480  wsuclem  33499  sltval2  33545  sltintdifex  33550  sltres  33551  nolt02o  33584  nogt01o  33585  bday1s  33711  lrold  33763  lrrecpo  33784  dfrdg4  33939  linedegen  34131  rankeq1o  34159  hfninf  34174  ordcmp  34322  curryset  34821  currysetlem3  34824  bj-projval  34872  bj-inftyexpitaudisj  35060  bj-inftyexpidisj  35065  irrdiff  35180  relowlpssretop  35221  finxpreclem2  35247  finxpreclem3  35250  finxpreclem5  35252  nlpineqsn  35265  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  mblfinlem1  35500  elpadd0  37509  pssn0  39856  oexpreposd  39969  diophin  40238  fiphp3d  40285  expdioph  40489  wepwsolem  40511  kelac1  40532  ensucne0  40762  relintabex  40806  brnonrel  40814  relexp01min  40939  iooinlbub  42655  stoweidlem34  43193  fourierdlem60  43325  fourierdlem61  43326  afv20defat  44339  spr0nelg  44544  sprsymrelfvlem  44558  fmtnoinf  44604  fmtno4prmfac193  44641  fmtno4prm  44643  31prm  44665  lighneallem3  44675  lighneallem4  44678  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  dig2nn1st  45567  itcoval1  45625  line2ylem  45713  ipolub00  45895