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  4059  nel02  4288  sbcel12  4372  sbcel2  4379  sbcbr123  5163  sbcbr  5164  axnul  5266  intex  5312  intnex  5313  iin0  5331  notsep  5332  nfcvb  5345  eunex  5359  opelopabsb  5512  brabv  5549  epelg  5560  0nelelxp  5694  elimasni  6091  onxpdisj  6489  ndmfvrcl  6915  canth  7371  oprssdm  7599  ndmovrcl  7604  omelon2  7879  poxp2  8145  xpord2indlem  8149  poxp3  8152  undefnel2  8280  tfr2b  8389  tz7.44-3  8401  nlim2  8481  ord1eln01  8487  ord2eln012  8488  1ellim  8489  2ellim  8490  eceqoveq  8826  2dom  9041  omxpenlem  9080  domunsn  9129  disjen  9136  infensuc  9157  ordfin  9214  0sdom1dom  9220  1sdom2dom  9228  infn0  9276  elfi2  9388  en3lp  9597  preleqALT  9600  rankxpsuc  9868  updjudhcoinrg  9942  sdomsdomcardi  9980  cardmin2  10008  pm54.43lem  10009  pr2ne  10012  alephgeom  10089  alephval3  10117  cfsuc  10263  cflim2  10269  alephval2  10585  axunnd  10609  canthp1lem1  10665  pwxpndom2  10678  rankcf  10790  pinq  10940  adderpq  10969  mulerpq  10970  nqpr  11027  ltsopr  11045  ltapr  11058  renepnf  11285  renemnf  11286  lt0ne0d  11807  prodgt0  12090  nnne0ALT  12302  nn0nepnf  12613  xrltnr  13174  pnfnlt  13183  nltmnf  13184  xrltnsym  13192  nltpnft  13220  ngtmnft  13222  xsubge0  13317  xmullem2  13321  xlemul1a  13344  xrsupsslem  13363  xrinfmsslem  13364  xrub  13368  fzpreddisj  13632  fzm1  13666  uzinf  14033  hashnemnf  14412  hashclb  14426  hasheq0  14431  hashnn0n0nn  14459  prprrab  14542  tpf1ofv1  14566  tpf1ofv2  14567  lsw0  14634  cats1un  14794  geolim  15963  geolim2  15964  georeclim  15965  geoisumr  15971  m1exp1  16472  bitsfzolem  16530  bitsfzo  16531  bitsinv1lem  16537  sadcp1  16551  saddisjlem  16560  smu01lem  16581  3prm  16790  pcgcd1  16975  pc2dvds  16977  pcmpt  16990  prmreclem5  17018  vdwap0  17074  prmo1  17135  fvprif  17653  setcepi  18183  oduclatb  18601  chnccats1  18719  chnccat  18720  smndex1n0mnd  19030  cntzrcl  19460  pmtrfrn  19591  pmtrprfval  19620  pmtrprfvalrn  19621  psgnunilem5  19627  odhash3  19709  gsumzaddlem  20054  gsumzsplit  20060  dprdcntz2  20173  trivnsimpgd  20232  0ringnnzr  20692  xrsdsreclblem  21632  dsmmfi  21957  islindf4  22057  mplcoe1  22259  mplcoe5  22262  psrbagsn  22285  pmatcollpw3fi1lem1  23017  istps  23165  haust1  23583  hauspwdom  23733  kqcldsat  23965  csdfil  24126  tsmssplit  24384  dscopn  24805  htpycc  25214  pco1  25249  pcohtpylem  25253  pcopt  25256  pcopt2  25257  pcoass  25258  pcorevlem  25260  itg11  25925  bddmulibl  26073  lhop1  26248  deg1nn0clb  26322  plypf1  26445  plyn0mulidp  26518  vieta1lem2  26550  logdmn0  26885  logcnlem3  26889  fsumharmonic  27256  sqff1o  27426  perfectlem1  27473  bposlem5  27532  lgsval2lem  27551  addsqrexnreu  27686  addsqnreup  27687  ostth  27883  ltsval2  27900  ltsintdifex  27905  ltsres  27906  nolt02o  27939  nogt01o  27940  bday1  28087  lrold  28170  lrrecpo  28214  mulsval  28382  legso  28949  axlowdimlem13  29419  axlowdimlem16  29422  axlowdim1  29424  axlowdim  29426  upgrfi  29556  lfgrnloop  29590  umgredgnlp  29612  wlkp1lem3  30141  rusgrnumwwlkl1  30447  clwwlk  30461  clwwlkn0  30506  clwwlknon1sn  30578  trlsegvdeg  30715  konigsberg  30745  ex-res  30929  norm1exi  31739  dmadjrnb  32395  strlem1  32739  largei  32756  ifeqeqx  33025  ubico  33254  expgt0b  33295  0ringirng  34207  rtelextdg2lem  34244  2sqr3minply  34298  dya2iocuni  34802  eulerpartlemgh  34897  ballotlem4  35018  signswch  35077  signstfvneq0  35088  signlem0  35103  xoromon  35601  fineqvomonb  35653  noinfepfnregs  35666  subfacp1lem1  35766  fmlaomn0  35977  gonan0  35979  goaln0  35980  fmla0disjsuc  35985  ex-sategoelelomsuc  36013  ex-sategoelel12  36014  prv1n  36018  bcneg1  36323  opelco3  36362  wsuclem  36410  dfrdg4  36538  linedegen  36731  rankeq1o  36759  hfninf  36774  ordcmp  37074  curryset  37698  currysetlem3  37701  bj-projval  37748  bj-inftyexpitaudisj  37965  bj-inftyexpidisj  37970  irrdiff  38086  relowlpssretop  38126  finxpreclem2  38152  finxpreclem3  38155  finxpreclem5  38157  nlpineqsn  38170  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  mblfinlem1  38414  suceldisj  39574  elpadd0  40690  pssn0  43105  oexpreposd  43205  diophin  43625  fiphp3d  43668  expdioph  43872  wepwsolem  43891  kelac1  43912  onov0suclim  44123  tfsconcatb0  44193  ensucne0  44377  relintabex  44429  brnonrel  44437  relexp01min  44561  iooinlbub  46339  stoweidlem34  46870  fourierdlem60  47002  fourierdlem61  47003  afv20defat  48128  minusmodnep2tmod  48255  spr0nelg  48384  sprsymrelfvlem  48398  fmtnoinf  48447  fmtno4prmfac193  48484  fmtno4prm  48486  31prm  48508  lighneallem3  48518  lighneallem4  48521  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  dig2nn1st  49543  itcoval1  49601  line2ylem  49689  ipolub00  49927  fucofvalne  50259