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 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  4039  nel02  4266  n0i  4267  sbcel12  4342  sbcel2  4349  sbcbr123  5128  sbcbr  5129  axnul  5229  intex  5261  intnex  5262  iin0  5284  notzfaus  5285  nfcvb  5299  eunex  5313  opelopabsb  5443  brabv  5482  epelg  5496  0nelelxp  5624  elimasni  5999  0ellim  6328  onxpdisj  6386  ndmfvrcl  6805  canth  7229  fvmptopabOLD  7330  oprssdm  7453  ndmovrcl  7458  omelon2  7725  undefnel2  8093  tfr2b  8227  tz7.44-3  8239  nlim2  8320  ord1eln01  8326  ord2eln012  8327  1ellim  8328  2ellim  8329  eceqoveq  8611  2dom  8820  omxpenlem  8860  domunsn  8914  disjen  8921  infensuc  8942  snnen2oOLD  9010  elfi2  9173  en3lp  9372  preleqALT  9375  rankxpsuc  9640  updjudhcoinrg  9691  sdomsdomcardi  9729  cardmin2  9757  pm54.43lem  9758  alephgeom  9838  alephval3  9866  cfsuc  10013  cflim2  10019  alephval2  10328  axunnd  10352  canthp1lem1  10408  pwxpndom2  10421  rankcf  10533  pinq  10683  adderpq  10712  mulerpq  10713  nqpr  10770  ltsopr  10788  ltapr  10801  renepnf  11023  renemnf  11024  lt0ne0d  11540  prodgt0  11822  nnne0ALT  12011  nn0nepnf  12313  xrltnr  12855  pnfnlt  12864  nltmnf  12865  xrltnsym  12871  nltpnft  12898  ngtmnft  12900  xsubge0  12995  xmullem2  12999  xlemul1a  13022  xrsupsslem  13041  xrinfmsslem  13042  xrub  13046  fzpreddisj  13305  fzm1  13336  uzinf  13685  hashnemnf  14058  hashclb  14073  hasheq0  14078  hashnn0n0nn  14106  prprrab  14187  lsw0  14268  cats1un  14434  geolim  15582  geolim2  15583  georeclim  15584  geoisumr  15590  m1exp1  16085  bitsfzolem  16141  bitsfzo  16142  bitsinv1lem  16148  sadcp1  16162  saddisjlem  16171  smu01lem  16192  3prm  16399  pcgcd1  16578  pc2dvds  16580  pcmpt  16593  prmreclem5  16621  vdwap0  16677  prmo1  16738  fvprif  17272  setcepi  17803  oduclatb  18225  smndex1n0mnd  18551  cntzrcl  18933  pmtrfrn  19066  pmtrprfval  19095  pmtrprfvalrn  19096  psgnunilem5  19102  odhash3  19181  gsumzaddlem  19522  gsumzsplit  19528  dprdcntz2  19641  trivnsimpgd  19700  0ringnnzr  20540  xrsdsreclblem  20644  dsmmfi  20945  islindf4  21045  mplcoe1  21238  mplcoe5  21241  psrbagsn  21271  pmatcollpw3fi1lem1  21935  istps  22083  haust1  22503  hauspwdom  22652  kqcldsat  22884  csdfil  23045  tsmssplit  23303  dscopn  23729  htpycc  24143  pco1  24178  pcohtpylem  24182  pcopt  24185  pcopt2  24186  pcoass  24187  pcorevlem  24189  itg11  24855  bddmulibl  25003  lhop1  25178  deg1nn0clb  25255  plypf1  25373  vieta1lem2  25471  logdmn0  25795  logcnlem3  25799  fsumharmonic  26161  sqff1o  26331  perfectlem1  26377  bposlem5  26436  lgsval2lem  26455  addsqrexnreu  26590  addsqnreup  26591  ostth  26787  legso  26960  axlowdimlem13  27322  axlowdimlem16  27325  axlowdim1  27327  axlowdim  27329  upgrfi  27461  lfgrnloop  27495  umgredgnlp  27517  wlkp1lem3  28043  rusgrnumwwlkl1  28333  clwwlk  28347  clwwlkn0  28392  clwwlknon1sn  28464  trlsegvdeg  28591  konigsberg  28621  ex-res  28805  norm1exi  29612  dmadjrnb  30268  strlem1  30612  largei  30629  ifeqeqx  30885  ubico  31096  dya2iocuni  32250  eulerpartlemgh  32345  ballotlem4  32465  plymulx0  32526  signswch  32540  signstfvneq0  32551  signlem0  32566  subfacp1lem1  33141  fmlaomn0  33352  gonan0  33354  goaln0  33355  fmla0disjsuc  33360  ex-sategoelelomsuc  33388  ex-sategoelel12  33389  prv1n  33393  bcneg1  33702  opelco3  33749  poxp2  33790  xpord2ind  33794  poxp3  33796  xpord3ind  33800  wsuclem  33819  sltval2  33859  sltintdifex  33864  sltres  33865  nolt02o  33898  nogt01o  33899  bday1s  34025  lrold  34077  lrrecpo  34098  dfrdg4  34253  linedegen  34445  rankeq1o  34473  hfninf  34488  ordcmp  34636  curryset  35135  currysetlem3  35138  bj-projval  35186  bj-inftyexpitaudisj  35376  bj-inftyexpidisj  35381  irrdiff  35497  relowlpssretop  35535  finxpreclem2  35561  finxpreclem3  35564  finxpreclem5  35566  nlpineqsn  35579  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  mblfinlem1  35814  elpadd0  37823  pssn0  40202  oexpreposd  40321  diophin  40594  fiphp3d  40641  expdioph  40845  wepwsolem  40867  kelac1  40888  ensucne0  41136  relintabex  41189  brnonrel  41197  relexp01min  41321  iooinlbub  43039  stoweidlem34  43575  fourierdlem60  43707  fourierdlem61  43708  afv20defat  44724  spr0nelg  44928  sprsymrelfvlem  44942  fmtnoinf  44988  fmtno4prmfac193  45025  fmtno4prm  45027  31prm  45049  lighneallem3  45059  lighneallem4  45062  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  dig2nn1st  45951  itcoval1  46009  line2ylem  46097  ipolub00  46279  tworepnotupword  46521