Theorem mtbiri 328

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

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

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 208

This theorem is referenced by:  psstr  4045  nel02  4274  sbcel12  4346  sbcel2  4353  sbcbr123  5133  sbcbr  5134  axnul  5234  intex  5279  intnex  5280  iin0  5298  notzfaus  5299  nfcvb  5312  eunex  5326  opelopabsb  5479  brabv  5515  epelg  5526  0nelelxp  5660  elimasni  6050  onxpdisj  6444  ndmfvrcl  6867  canth  7317  oprssdm  7544  ndmovrcl  7549  omelon2  7826  poxp2  8090  xpord2indlem  8094  poxp3  8097  undefnel2  8224  tfr2b  8332  tz7.44-3  8344  nlim2  8422  ord1eln01  8428  ord2eln012  8429  1ellim  8430  2ellim  8431  eceqoveq  8766  2dom  8974  omxpenlem  9013  domunsn  9062  disjen  9069  infensuc  9090  ordfin  9147  0sdom1dom  9153  1sdom2dom  9161  infn0  9209  elfi2  9324  en3lp  9533  preleqALT  9536  rankxpsuc  9804  updjudhcoinrg  9855  sdomsdomcardi  9893  cardmin2  9921  pm54.43lem  9922  pr2ne  9925  alephgeom  10002  alephval3  10030  cfsuc  10177  cflim2  10183  alephval2  10493  axunnd  10517  canthp1lem1  10573  pwxpndom2  10586  rankcf  10698  pinq  10848  adderpq  10877  mulerpq  10878  nqpr  10935  ltsopr  10953  ltapr  10966  renepnf  11191  renemnf  11192  lt0ne0d  11713  prodgt0  12000  nnne0ALT  12213  nn0nepnf  12516  xrltnr  13068  pnfnlt  13077  nltmnf  13078  xrltnsym  13086  nltpnft  13114  ngtmnft  13116  xsubge0  13211  xmullem2  13215  xlemul1a  13238  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  fzpreddisj  13525  fzm1  13559  uzinf  13925  hashnemnf  14304  hashclb  14318  hasheq0  14323  hashnn0n0nn  14351  prprrab  14433  tpf1ofv1  14457  tpf1ofv2  14458  lsw0  14525  cats1un  14681  geolim  15833  geolim2  15834  georeclim  15835  geoisumr  15841  m1exp1  16343  bitsfzolem  16401  bitsfzo  16402  bitsinv1lem  16408  sadcp1  16422  saddisjlem  16431  smu01lem  16452  3prm  16661  pcgcd1  16846  pc2dvds  16848  pcmpt  16861  prmreclem5  16889  vdwap0  16945  prmo1  17006  fvprif  17523  setcepi  18053  oduclatb  18471  chnccats1  18589  chnccat  18590  smndex1n0mnd  18881  cntzrcl  19300  pmtrfrn  19431  pmtrprfval  19460  pmtrprfvalrn  19461  psgnunilem5  19467  odhash3  19549  gsumzaddlem  19894  gsumzsplit  19900  dprdcntz2  20013  trivnsimpgd  20072  0ringnnzr  20504  xrsdsreclblem  21395  dsmmfi  21720  islindf4  21820  mplcoe1  22020  mplcoe5  22023  psrbagsn  22046  pmatcollpw3fi1lem1  22776  istps  22924  haust1  23342  hauspwdom  23491  kqcldsat  23723  csdfil  23884  tsmssplit  24142  dscopn  24563  htpycc  24972  pco1  25007  pcohtpylem  25011  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  itg11  25683  bddmulibl  25831  lhop1  26006  deg1nn0clb  26080  plypf1  26202  vieta1lem2  26302  logdmn0  26629  logcnlem3  26633  fsumharmonic  27000  sqff1o  27170  perfectlem1  27217  bposlem5  27276  lgsval2lem  27295  addsqrexnreu  27430  addsqnreup  27431  ostth  27627  ltsval2  27645  ltsintdifex  27650  ltsres  27651  nolt02o  27684  nogt01o  27685  bday1  27831  lrold  27914  lrrecpo  27958  mulsval  28126  legso  28692  axlowdimlem13  29048  axlowdimlem16  29051  axlowdim1  29053  axlowdim  29055  upgrfi  29185  lfgrnloop  29219  umgredgnlp  29241  wlkp1lem3  29767  rusgrnumwwlkl1  30064  clwwlk  30078  clwwlkn0  30123  clwwlknon1sn  30195  trlsegvdeg  30322  konigsberg  30352  ex-res  30536  norm1exi  31346  dmadjrnb  32002  strlem1  32346  largei  32363  ifeqeqx  32637  ubico  32874  expgt0b  32916  0ringirng  33880  rtelextdg2lem  33917  2sqr3minply  33971  dya2iocuni  34474  eulerpartlemgh  34569  ballotlem4  34690  plymulx0  34738  signswch  34752  signstfvneq0  34763  signlem0  34778  xoromon  35277  fineqvomonb  35307  noinfepfnregs  35320  subfacp1lem1  35414  fmlaomn0  35625  gonan0  35627  goaln0  35628  fmla0disjsuc  35633  ex-sategoelelomsuc  35661  ex-sategoelel12  35662  prv1n  35666  bcneg1  35971  opelco3  36010  wsuclem  36058  dfrdg4  36186  linedegen  36378  rankeq1o  36406  hfninf  36421  ordcmp  36682  curryset  37306  currysetlem3  37309  bj-projval  37356  bj-inftyexpitaudisj  37572  bj-inftyexpidisj  37577  irrdiff  37693  relowlpssretop  37733  finxpreclem2  37759  finxpreclem3  37762  finxpreclem5  37764  nlpineqsn  37777  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  mblfinlem1  38031  suceldisj  39192  elpadd0  40308  pssn0  42721  oexpreposd  42806  diophin  43228  fiphp3d  43271  expdioph  43475  wepwsolem  43494  kelac1  43515  onov0suclim  43726  tfsconcatb0  43796  ensucne0  43980  relintabex  44032  brnonrel  44040  relexp01min  44164  iooinlbub  45953  stoweidlem34  46484  fourierdlem60  46616  fourierdlem61  46617  afv20defat  47702  minusmodnep2tmod  47829  spr0nelg  47958  sprsymrelfvlem  47972  fmtnoinf  48021  fmtno4prmfac193  48058  fmtno4prm  48060  31prm  48082  lighneallem3  48092  lighneallem4  48095  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  dig2nn1st  49103  itcoval1  49161  line2ylem  49249  ipolub00  49490  fucofvalne  49822