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 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  psstr  4061  nel02  4291  sbcel12  4375  sbcel2  4382  sbcbr123  5164  sbcbr  5165  axnul  5267  intex  5313  intnex  5314  iin0  5332  notsep  5333  nfcvb  5346  eunex  5360  opelopabsb  5513  brabv  5550  epelg  5561  0nelelxp  5695  elimasni  6092  onxpdisj  6488  ndmfvrcl  6914  canth  7366  oprssdm  7593  ndmovrcl  7598  omelon2  7873  poxp2  8137  xpord2indlem  8141  poxp3  8144  undefnel2  8272  tfr2b  8381  tz7.44-3  8393  nlim2  8473  ord1eln01  8479  ord2eln012  8480  1ellim  8481  2ellim  8482  eceqoveq  8818  2dom  9025  omxpenlem  9064  domunsn  9113  disjen  9120  infensuc  9141  ordfin  9198  0sdom1dom  9204  1sdom2dom  9212  infn0  9260  elfi2  9372  en3lp  9581  preleqALT  9584  rankxpsuc  9852  updjudhcoinrg  9926  sdomsdomcardi  9964  cardmin2  9992  pm54.43lem  9993  pr2ne  9996  alephgeom  10073  alephval3  10101  cfsuc  10247  cflim2  10253  alephval2  10563  axunnd  10587  canthp1lem1  10643  pwxpndom2  10656  rankcf  10768  pinq  10918  adderpq  10947  mulerpq  10948  nqpr  11005  ltsopr  11023  ltapr  11036  renepnf  11263  renemnf  11264  lt0ne0d  11785  prodgt0  12068  nnne0ALT  12280  nn0nepnf  12591  xrltnr  13150  pnfnlt  13159  nltmnf  13160  xrltnsym  13168  nltpnft  13196  ngtmnft  13198  xsubge0  13293  xmullem2  13297  xlemul1a  13320  xrsupsslem  13339  xrinfmsslem  13340  xrub  13344  fzpreddisj  13608  fzm1  13642  uzinf  14008  hashnemnf  14387  hashclb  14401  hasheq0  14406  hashnn0n0nn  14434  prprrab  14517  tpf1ofv1  14541  tpf1ofv2  14542  lsw0  14609  cats1un  14765  geolim  15931  geolim2  15932  georeclim  15933  geoisumr  15939  m1exp1  16440  bitsfzolem  16498  bitsfzo  16499  bitsinv1lem  16505  sadcp1  16519  saddisjlem  16528  smu01lem  16549  3prm  16758  pcgcd1  16943  pc2dvds  16945  pcmpt  16958  prmreclem5  16986  vdwap0  17042  prmo1  17103  fvprif  17621  setcepi  18151  oduclatb  18569  chnccats1  18687  chnccat  18688  smndex1n0mnd  18980  cntzrcl  19403  pmtrfrn  19534  pmtrprfval  19563  pmtrprfvalrn  19564  psgnunilem5  19570  odhash3  19652  gsumzaddlem  19997  gsumzsplit  20003  dprdcntz2  20116  trivnsimpgd  20175  0ringnnzr  20634  xrsdsreclblem  21574  dsmmfi  21899  islindf4  21999  mplcoe1  22199  mplcoe5  22202  psrbagsn  22225  pmatcollpw3fi1lem1  22954  istps  23102  haust1  23520  hauspwdom  23669  kqcldsat  23901  csdfil  24062  tsmssplit  24320  dscopn  24741  htpycc  25150  pco1  25185  pcohtpylem  25189  pcopt  25192  pcopt2  25193  pcoass  25194  pcorevlem  25196  itg11  25861  bddmulibl  26009  lhop1  26184  deg1nn0clb  26258  plypf1  26380  plyn0mulidp  26453  vieta1lem2  26483  logdmn0  26816  logcnlem3  26820  fsumharmonic  27187  sqff1o  27357  perfectlem1  27404  bposlem5  27463  lgsval2lem  27482  addsqrexnreu  27617  addsqnreup  27618  ostth  27814  ltsval2  27831  ltsintdifex  27836  ltsres  27837  nolt02o  27870  nogt01o  27871  bday1  28018  lrold  28101  lrrecpo  28145  mulsval  28313  legso  28879  axlowdimlem13  29315  axlowdimlem16  29318  axlowdim1  29320  axlowdim  29322  upgrfi  29452  lfgrnloop  29486  umgredgnlp  29508  wlkp1lem3  30034  rusgrnumwwlkl1  30331  clwwlk  30345  clwwlkn0  30390  clwwlknon1sn  30462  trlsegvdeg  30589  konigsberg  30619  ex-res  30803  norm1exi  31613  dmadjrnb  32269  strlem1  32613  largei  32630  ifeqeqx  32899  ubico  33131  expgt0b  33172  0ringirng  34088  rtelextdg2lem  34125  2sqr3minply  34179  dya2iocuni  34682  eulerpartlemgh  34777  ballotlem4  34898  signswch  34957  signstfvneq0  34968  signlem0  34983  xoromon  35488  fineqvomonb  35540  noinfepfnregs  35553  subfacp1lem1  35679  fmlaomn0  35890  gonan0  35892  goaln0  35893  fmla0disjsuc  35898  ex-sategoelelomsuc  35926  ex-sategoelel12  35927  prv1n  35931  bcneg1  36236  opelco3  36275  wsuclem  36323  dfrdg4  36451  linedegen  36643  rankeq1o  36671  hfninf  36686  ordcmp  36986  curryset  37610  currysetlem3  37613  bj-projval  37660  bj-inftyexpitaudisj  37877  bj-inftyexpidisj  37882  irrdiff  37998  relowlpssretop  38038  finxpreclem2  38064  finxpreclem3  38067  finxpreclem5  38069  nlpineqsn  38082  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  mblfinlem1  38336  suceldisj  39495  elpadd0  40611  pssn0  43026  oexpreposd  43111  diophin  43531  fiphp3d  43574  expdioph  43778  wepwsolem  43797  kelac1  43818  onov0suclim  44029  tfsconcatb0  44099  ensucne0  44283  relintabex  44335  brnonrel  44343  relexp01min  44467  iooinlbub  46245  stoweidlem34  46776  fourierdlem60  46908  fourierdlem61  46909  afv20defat  47997  minusmodnep2tmod  48124  spr0nelg  48253  sprsymrelfvlem  48267  fmtnoinf  48316  fmtno4prmfac193  48353  fmtno4prm  48355  31prm  48377  lighneallem3  48387  lighneallem4  48390  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  dig2nn1st  49413  itcoval1  49471  line2ylem  49559  ipolub00  49799  fucofvalne  50131