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

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

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 210

This theorem is referenced by:  psstr  4063  nel02  4293  sbcel12  4377  sbcel2  4384  sbcbr123  5166  sbcbr  5167  axnul  5269  intex  5316  intnex  5317  iin0  5335  notsep  5336  nfcvb  5349  eunex  5363  opelopabsb  5516  brabv  5553  epelg  5564  0nelelxp  5698  elimasni  6095  onxpdisj  6490  ndmfvrcl  6916  canth  7366  oprssdm  7593  ndmovrcl  7598  omelon2  7876  poxp2  8140  xpord2indlem  8144  poxp3  8147  undefnel2  8275  tfr2b  8384  tz7.44-3  8396  nlim2  8476  ord1eln01  8482  ord2eln012  8483  1ellim  8484  2ellim  8485  eceqoveq  8821  2dom  9028  omxpenlem  9067  domunsn  9116  disjen  9123  infensuc  9144  ordfin  9201  0sdom1dom  9207  1sdom2dom  9215  infn0  9263  elfi2  9375  en3lp  9584  preleqALT  9587  rankxpsuc  9855  updjudhcoinrg  9920  sdomsdomcardi  9958  cardmin2  9986  pm54.43lem  9987  pr2ne  9990  alephgeom  10067  alephval3  10095  cfsuc  10242  cflim2  10248  alephval2  10558  axunnd  10582  canthp1lem1  10638  pwxpndom2  10651  rankcf  10763  pinq  10913  adderpq  10942  mulerpq  10943  nqpr  11000  ltsopr  11018  ltapr  11031  renepnf  11258  renemnf  11259  lt0ne0d  11780  prodgt0  12063  nnne0ALT  12275  nn0nepnf  12586  xrltnr  13145  pnfnlt  13154  nltmnf  13155  xrltnsym  13163  nltpnft  13191  ngtmnft  13193  xsubge0  13288  xmullem2  13292  xlemul1a  13315  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  fzpreddisj  13603  fzm1  13637  uzinf  14003  hashnemnf  14382  hashclb  14396  hasheq0  14401  hashnn0n0nn  14429  prprrab  14512  tpf1ofv1  14536  tpf1ofv2  14537  lsw0  14604  cats1un  14760  geolim  15926  geolim2  15927  georeclim  15928  geoisumr  15934  m1exp1  16435  bitsfzolem  16493  bitsfzo  16494  bitsinv1lem  16500  sadcp1  16514  saddisjlem  16523  smu01lem  16544  3prm  16753  pcgcd1  16938  pc2dvds  16940  pcmpt  16953  prmreclem5  16981  vdwap0  17037  prmo1  17098  fvprif  17616  setcepi  18146  oduclatb  18564  chnccats1  18682  chnccat  18683  smndex1n0mnd  18975  cntzrcl  19398  pmtrfrn  19529  pmtrprfval  19558  pmtrprfvalrn  19559  psgnunilem5  19565  odhash3  19647  gsumzaddlem  19992  gsumzsplit  19998  dprdcntz2  20111  trivnsimpgd  20170  0ringnnzr  20610  xrsdsreclblem  21544  dsmmfi  21869  islindf4  21969  mplcoe1  22169  mplcoe5  22172  psrbagsn  22195  pmatcollpw3fi1lem1  22924  istps  23072  haust1  23490  hauspwdom  23639  kqcldsat  23871  csdfil  24032  tsmssplit  24290  dscopn  24711  htpycc  25120  pco1  25155  pcohtpylem  25159  pcopt  25162  pcopt2  25163  pcoass  25164  pcorevlem  25166  itg11  25831  bddmulibl  25979  lhop1  26154  deg1nn0clb  26228  plypf1  26350  plyn0mulidp  26423  vieta1lem2  26453  logdmn0  26783  logcnlem3  26787  fsumharmonic  27154  sqff1o  27324  perfectlem1  27371  bposlem5  27430  lgsval2lem  27449  addsqrexnreu  27584  addsqnreup  27585  ostth  27781  ltsval2  27798  ltsintdifex  27803  ltsres  27804  nolt02o  27837  nogt01o  27838  bday1  27985  lrold  28068  lrrecpo  28112  mulsval  28280  legso  28846  axlowdimlem13  29282  axlowdimlem16  29285  axlowdim1  29287  axlowdim  29289  upgrfi  29419  lfgrnloop  29453  umgredgnlp  29475  wlkp1lem3  30001  rusgrnumwwlkl1  30298  clwwlk  30312  clwwlkn0  30357  clwwlknon1sn  30429  trlsegvdeg  30556  konigsberg  30586  ex-res  30770  norm1exi  31580  dmadjrnb  32236  strlem1  32580  largei  32597  ifeqeqx  32866  ubico  33098  expgt0b  33139  0ringirng  34057  rtelextdg2lem  34094  2sqr3minply  34148  dya2iocuni  34651  eulerpartlemgh  34746  ballotlem4  34867  signswch  34926  signstfvneq0  34937  signlem0  34952  xoromon  35457  fineqvomonb  35510  noinfepfnregs  35523  subfacp1lem1  35649  fmlaomn0  35860  gonan0  35862  goaln0  35863  fmla0disjsuc  35868  ex-sategoelelomsuc  35896  ex-sategoelel12  35897  prv1n  35901  bcneg1  36206  opelco3  36245  wsuclem  36293  dfrdg4  36421  linedegen  36613  rankeq1o  36641  hfninf  36656  ordcmp  36936  curryset  37560  currysetlem3  37563  bj-projval  37610  bj-inftyexpitaudisj  37827  bj-inftyexpidisj  37832  irrdiff  37948  relowlpssretop  37988  finxpreclem2  38014  finxpreclem3  38017  finxpreclem5  38019  nlpineqsn  38032  poimirlem18  38267  poimirlem19  38268  poimirlem20  38269  mblfinlem1  38286  suceldisj  39445  elpadd0  40561  pssn0  42976  oexpreposd  43061  diophin  43483  fiphp3d  43526  expdioph  43730  wepwsolem  43749  kelac1  43770  onov0suclim  43981  tfsconcatb0  44051  ensucne0  44235  relintabex  44287  brnonrel  44295  relexp01min  44419  iooinlbub  46197  stoweidlem34  46728  fourierdlem60  46860  fourierdlem61  46861  afv20defat  47946  minusmodnep2tmod  48073  spr0nelg  48202  sprsymrelfvlem  48216  fmtnoinf  48265  fmtno4prmfac193  48302  fmtno4prm  48304  31prm  48326  lighneallem3  48336  lighneallem4  48339  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  dig2nn1st  49362  itcoval1  49420  line2ylem  49508  ipolub00  49748  fucofvalne  50080