Theorem mtbiri 319

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

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

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 199

This theorem is referenced by:  psstr  3970  n0i  4184  sbcel12  4244  sbcel2  4251  sbcbr123  4981  sbcbr  4982  axnul  5064  intex  5094  intnex  5095  iin0  5113  nfcvb  5128  eunex  5141  opelopabsb  5268  brabv  5302  epelg  5315  0nelelxp  5439  elimasni  5794  0ellim  6089  onxpdisj  6146  ndmfvrcl  6528  canth  6932  fvmptopab  7026  oprssdm  7143  ndmovrcl  7148  omelon2  7406  undefnel2  7743  tfr2b  7833  tz7.44-3  7845  eceqoveq  8198  2dom  8375  omxpenlem  8410  domunsn  8459  disjen  8466  infensuc  8487  snnen2o  8498  elfi2  8669  en3lp  8867  preleqALT  8870  rankxpsuc  9101  updjudhcoinrg  9152  sdomsdomcardi  9190  cardmin2  9217  pm54.43lem  9218  alephgeom  9298  alephval3  9326  cfsuc  9473  cflim2  9479  alephval2  9788  axunnd  9812  canthp1lem1  9868  pwxpndom2  9881  rankcf  9993  pinq  10143  adderpq  10172  mulerpq  10173  nqpr  10230  ltsopr  10248  ltapr  10261  renepnf  10484  renemnf  10485  lt0ne0d  11002  prodgt0  11284  nnne0ALT  11475  nn0nepnf  11784  xrltnr  12328  pnfnlt  12337  nltmnf  12338  xrltnsym  12344  nltpnft  12371  ngtmnft  12373  xsubge0  12467  xmullem2  12471  xlemul1a  12494  xrsupsslem  12513  xrinfmsslem  12514  xrub  12518  fzpreddisj  12769  fzm1  12800  uzinf  13145  hashnemnf  13516  hashclb  13531  hasheq0  13536  hashnn0n0nn  13562  prprrab  13636  lsw0  13722  cats1un  13908  geolim  15080  geolim2  15081  georeclim  15082  geoisumr  15088  m1exp1  15581  bitsfzolem  15637  bitsfzo  15638  bitsinv1lem  15644  sadcp1  15658  saddisjlem  15667  smu01lem  15688  3prm  15888  pcgcd1  16063  pc2dvds  16065  pcmpt  16078  prmreclem5  16106  vdwap0  16162  prmo1  16223  setcepi  17200  oduclatb  17606  cntzrcl  18222  pmtrfrn  18341  pmtrprfval  18370  pmtrprfvalrn  18371  psgnunilem5  18377  psgnunilem5OLD  18378  odhash3  18456  gsumzaddlem  18788  gsumzsplit  18794  dprdcntz2  18904  0ringnnzr  19757  mplcoe1  19953  mplcoe5  19956  psrbagsn  19982  xrsdsreclblem  20287  dsmmbas2  20577  dsmmfi  20578  islindf4  20678  pmatcollpw3fi1lem1  21092  istps  21240  haust1  21658  hauspwdom  21807  kqcldsat  22039  csdfil  22200  tsmssplit  22457  dscopn  22880  htpycc  23281  pco1  23316  pcohtpylem  23320  pcopt  23323  pcopt2  23324  pcoass  23325  pcorevlem  23327  itg11  23989  bddmulibl  24136  lhop1  24308  deg1nn0clb  24381  plypf1  24499  vieta1lem2  24597  logdmn0  24918  logcnlem3  24922  fsumharmonic  25285  sqff1o  25455  perfectlem1  25501  bposlem5  25560  lgsval2lem  25579  addsqrexnreu  25714  addsqnreup  25715  ostth  25911  legso  26081  axlowdimlem13  26437  axlowdimlem16  26440  axlowdim1  26442  axlowdim  26444  upgrfi  26573  lfgrnloop  26607  umgredgnlp  26629  wlkp1lem3  27157  rusgrnumwwlkl1  27468  clwwlk  27483  clwwlkn0  27537  clwwlknon1sn  27622  trlsegvdeg  27751  konigsberg  27783  ex-res  27992  norm1exi  28800  dmadjrnb  29458  strlem1  29802  largei  29819  ifeqeqx  30059  ubico  30244  dya2iocuni  31177  eulerpartlemgh  31272  ballotlem4  31393  plymulx0  31454  signswch  31468  signstfvneq0  31480  signlem0  31496  subfacp1lem1  32001  bcneg1  32458  opelco3  32508  wsuclem  32603  sltval2  32654  sltintdifex  32659  sltres  32660  nolt02o  32690  dfrdg4  32903  linedegen  33095  rankeq1o  33123  hfninf  33138  ordcmp  33285  bj-eunex  33597  bj-projval  33791  bj-inftyexpitaudisj  33921  bj-inftyexpidisj  33926  relowlpssretop  34052  finxpreclem2  34077  finxpreclem3  34080  finxpreclem5  34082  nlpineqsn  34095  poimirlem18  34329  poimirlem19  34330  poimirlem20  34331  mblfinlem1  34348  nel02  35005  elpadd0  36368  pssn0  38536  oexpreposd  38589  diophin  38743  fiphp3d  38790  expdioph  38994  wepwsolem  39016  kelac1  39037  relintabex  39281  brnonrel  39289  relexp01min  39399  trivnsimpgd  40009  iooinlbub  41186  stoweidlem34  41729  fourierdlem60  41861  fourierdlem61  41862  afv20defat  42816  spr0nelg  42980  sprsymrelfvlem  42994  fmtnoinf  43040  fmtno4prmfac193  43077  fmtno4prm  43079  31prm  43102  lighneallem3  43114  lighneallem4  43117  nnsum4primeseven  43307  nnsum4primesevenALTV  43308  dig2nn1st  44007  line2ylem  44080