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

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

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 207

This theorem is referenced by:  psstr  4082  nel02  4314  n0i  4315  sbcel12  4386  sbcel2  4393  sbcbr123  5173  sbcbr  5174  axnul  5275  intex  5314  intnex  5315  iin0  5332  notzfaus  5333  nfcvb  5346  eunex  5360  opelopabsb  5505  brabv  5543  epelg  5554  0nelelxp  5689  elimasni  6078  0ellim  6416  onxpdisj  6479  ndmfvrcl  6911  canth  7357  fvmptopabOLD  7460  oprssdm  7586  ndmovrcl  7591  omelon2  7872  poxp2  8140  xpord2indlem  8144  poxp3  8147  undefnel2  8274  tfr2b  8408  tz7.44-3  8420  nlim2  8500  ord1eln01  8506  ord2eln012  8507  1ellim  8508  2ellim  8509  eceqoveq  8834  2dom  9042  omxpenlem  9085  domunsn  9139  disjen  9146  infensuc  9167  snnen2oOLD  9234  0sdom1dom  9244  1sdom2dom  9253  infn0  9310  elfi2  9424  en3lp  9626  preleqALT  9629  rankxpsuc  9894  updjudhcoinrg  9945  sdomsdomcardi  9983  cardmin2  10011  pm54.43lem  10012  pr2ne  10016  alephgeom  10094  alephval3  10122  cfsuc  10269  cflim2  10275  alephval2  10584  axunnd  10608  canthp1lem1  10664  pwxpndom2  10677  rankcf  10789  pinq  10939  adderpq  10968  mulerpq  10969  nqpr  11026  ltsopr  11044  ltapr  11057  renepnf  11281  renemnf  11282  lt0ne0d  11800  prodgt0  12086  nnne0ALT  12276  nn0nepnf  12580  xrltnr  13133  pnfnlt  13142  nltmnf  13143  xrltnsym  13151  nltpnft  13178  ngtmnft  13180  xsubge0  13275  xmullem2  13279  xlemul1a  13302  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  fzpreddisj  13588  fzm1  13622  uzinf  13981  hashnemnf  14360  hashclb  14374  hasheq0  14379  hashnn0n0nn  14407  prprrab  14489  tpf1ofv1  14513  tpf1ofv2  14514  lsw0  14581  cats1un  14737  geolim  15884  geolim2  15885  georeclim  15886  geoisumr  15892  m1exp1  16393  bitsfzolem  16451  bitsfzo  16452  bitsinv1lem  16458  sadcp1  16472  saddisjlem  16481  smu01lem  16502  3prm  16711  pcgcd1  16895  pc2dvds  16897  pcmpt  16910  prmreclem5  16938  vdwap0  16994  prmo1  17055  fvprif  17573  setcepi  18099  oduclatb  18515  smndex1n0mnd  18888  cntzrcl  19308  pmtrfrn  19437  pmtrprfval  19466  pmtrprfvalrn  19467  psgnunilem5  19473  odhash3  19555  gsumzaddlem  19900  gsumzsplit  19906  dprdcntz2  20019  trivnsimpgd  20078  0ringnnzr  20483  xrsdsreclblem  21378  dsmmfi  21696  islindf4  21796  mplcoe1  21993  mplcoe5  21996  psrbagsn  22019  pmatcollpw3fi1lem1  22722  istps  22870  haust1  23288  hauspwdom  23437  kqcldsat  23669  csdfil  23830  tsmssplit  24088  dscopn  24510  htpycc  24928  pco1  24964  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  itg11  25642  bddmulibl  25790  lhop1  25969  deg1nn0clb  26045  plypf1  26167  vieta1lem2  26269  logdmn0  26599  logcnlem3  26603  fsumharmonic  26972  sqff1o  27142  perfectlem1  27190  bposlem5  27249  lgsval2lem  27268  addsqrexnreu  27403  addsqnreup  27404  ostth  27600  sltval2  27618  sltintdifex  27623  sltres  27624  nolt02o  27657  nogt01o  27658  bday1s  27793  lrold  27852  lrrecpo  27891  mulsval  28052  legso  28524  axlowdimlem13  28879  axlowdimlem16  28882  axlowdim1  28884  axlowdim  28886  upgrfi  29016  lfgrnloop  29050  umgredgnlp  29072  wlkp1lem3  29601  rusgrnumwwlkl1  29896  clwwlk  29910  clwwlkn0  29955  clwwlknon1sn  30027  trlsegvdeg  30154  konigsberg  30184  ex-res  30368  norm1exi  31177  dmadjrnb  31833  strlem1  32177  largei  32194  ifeqeqx  32469  ubico  32698  expgt0b  32741  chnccats1  32941  0ringirng  33676  rtelextdg2lem  33706  2sqr3minply  33760  dya2iocuni  34261  eulerpartlemgh  34356  ballotlem4  34477  plymulx0  34525  signswch  34539  signstfvneq0  34550  signlem0  34565  subfacp1lem1  35147  fmlaomn0  35358  gonan0  35360  goaln0  35361  fmla0disjsuc  35366  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv1n  35399  bcneg1  35699  opelco3  35738  wsuclem  35789  dfrdg4  35915  linedegen  36107  rankeq1o  36135  hfninf  36150  ordcmp  36411  curryset  36910  currysetlem3  36913  bj-projval  36960  bj-inftyexpitaudisj  37169  bj-inftyexpidisj  37174  irrdiff  37290  relowlpssretop  37328  finxpreclem2  37354  finxpreclem3  37357  finxpreclem5  37359  nlpineqsn  37372  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  mblfinlem1  37627  elpadd0  39774  pssn0  42224  oexpreposd  42318  diophin  42742  fiphp3d  42789  expdioph  42994  wepwsolem  43013  kelac1  43034  onov0suclim  43245  tfsconcatb0  43315  ensucne0  43500  relintabex  43552  brnonrel  43560  relexp01min  43684  iooinlbub  45478  stoweidlem34  46011  fourierdlem60  46143  fourierdlem61  46144  tworepnotupword  46863  afv20defat  47209  minusmodnep2tmod  47330  spr0nelg  47438  sprsymrelfvlem  47452  fmtnoinf  47498  fmtno4prmfac193  47535  fmtno4prm  47537  31prm  47559  lighneallem3  47569  lighneallem4  47572  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  dig2nn1st  48533  itcoval1  48591  line2ylem  48679  ipolub00  48915  fucofvalne  49184