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  4065  nel02  4295  sbcel12  4379  sbcel2  4386  sbcbr123  5170  sbcbr  5171  axnul  5273  intex  5319  intnex  5320  iin0  5338  notsep  5339  nfcvb  5352  eunex  5366  opelopabsb  5519  brabv  5556  epelg  5567  0nelelxp  5701  elimasni  6098  onxpdisj  6495  ndmfvrcl  6921  canth  7377  oprssdm  7604  ndmovrcl  7609  omelon2  7884  poxp2  8148  xpord2indlem  8152  poxp3  8155  undefnel2  8283  tfr2b  8392  tz7.44-3  8404  nlim2  8484  ord1eln01  8490  ord2eln012  8491  1ellim  8492  2ellim  8493  eceqoveq  8829  2dom  9037  omxpenlem  9076  domunsn  9125  disjen  9132  infensuc  9153  ordfin  9210  0sdom1dom  9216  1sdom2dom  9224  infn0  9272  elfi2  9384  en3lp  9593  preleqALT  9596  rankxpsuc  9864  updjudhcoinrg  9938  sdomsdomcardi  9976  cardmin2  10004  pm54.43lem  10005  pr2ne  10008  alephgeom  10085  alephval3  10113  cfsuc  10259  cflim2  10265  alephval2  10575  axunnd  10599  canthp1lem1  10655  pwxpndom2  10668  rankcf  10780  pinq  10930  adderpq  10959  mulerpq  10960  nqpr  11017  ltsopr  11035  ltapr  11048  renepnf  11275  renemnf  11276  lt0ne0d  11797  prodgt0  12080  nnne0ALT  12292  nn0nepnf  12603  xrltnr  13162  pnfnlt  13171  nltmnf  13172  xrltnsym  13180  nltpnft  13208  ngtmnft  13210  xsubge0  13305  xmullem2  13309  xlemul1a  13332  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  fzpreddisj  13620  fzm1  13654  uzinf  14021  hashnemnf  14400  hashclb  14414  hasheq0  14419  hashnn0n0nn  14447  prprrab  14530  tpf1ofv1  14554  tpf1ofv2  14555  lsw0  14622  cats1un  14782  geolim  15950  geolim2  15951  georeclim  15952  geoisumr  15958  m1exp1  16459  bitsfzolem  16517  bitsfzo  16518  bitsinv1lem  16524  sadcp1  16538  saddisjlem  16547  smu01lem  16568  3prm  16777  pcgcd1  16962  pc2dvds  16964  pcmpt  16977  prmreclem5  17005  vdwap0  17061  prmo1  17122  fvprif  17640  setcepi  18170  oduclatb  18588  chnccats1  18706  chnccat  18707  smndex1n0mnd  19005  cntzrcl  19428  pmtrfrn  19559  pmtrprfval  19588  pmtrprfvalrn  19589  psgnunilem5  19595  odhash3  19677  gsumzaddlem  20022  gsumzsplit  20028  dprdcntz2  20141  trivnsimpgd  20200  0ringnnzr  20660  xrsdsreclblem  21600  dsmmfi  21925  islindf4  22025  mplcoe1  22225  mplcoe5  22228  psrbagsn  22251  pmatcollpw3fi1lem1  22980  istps  23128  haust1  23546  hauspwdom  23695  kqcldsat  23927  csdfil  24088  tsmssplit  24346  dscopn  24767  htpycc  25176  pco1  25211  pcohtpylem  25215  pcopt  25218  pcopt2  25219  pcoass  25220  pcorevlem  25222  itg11  25887  bddmulibl  26035  lhop1  26210  deg1nn0clb  26284  plypf1  26406  plyn0mulidp  26479  vieta1lem2  26509  logdmn0  26842  logcnlem3  26846  fsumharmonic  27213  sqff1o  27383  perfectlem1  27430  bposlem5  27489  lgsval2lem  27508  addsqrexnreu  27643  addsqnreup  27644  ostth  27840  ltsval2  27857  ltsintdifex  27862  ltsres  27863  nolt02o  27896  nogt01o  27897  bday1  28044  lrold  28127  lrrecpo  28171  mulsval  28339  legso  28905  axlowdimlem13  29341  axlowdimlem16  29344  axlowdim1  29346  axlowdim  29348  upgrfi  29478  lfgrnloop  29512  umgredgnlp  29534  wlkp1lem3  30060  rusgrnumwwlkl1  30357  clwwlk  30371  clwwlkn0  30416  clwwlknon1sn  30488  trlsegvdeg  30615  konigsberg  30645  ex-res  30829  norm1exi  31639  dmadjrnb  32295  strlem1  32639  largei  32656  ifeqeqx  32925  ubico  33157  expgt0b  33198  0ringirng  34110  rtelextdg2lem  34147  2sqr3minply  34201  dya2iocuni  34704  eulerpartlemgh  34799  ballotlem4  34920  signswch  34979  signstfvneq0  34990  signlem0  35005  xoromon  35503  fineqvomonb  35555  noinfepfnregs  35568  subfacp1lem1  35691  fmlaomn0  35902  gonan0  35904  goaln0  35905  fmla0disjsuc  35910  ex-sategoelelomsuc  35938  ex-sategoelel12  35939  prv1n  35943  bcneg1  36248  opelco3  36287  wsuclem  36335  dfrdg4  36463  linedegen  36655  rankeq1o  36683  hfninf  36698  ordcmp  36998  curryset  37622  currysetlem3  37625  bj-projval  37672  bj-inftyexpitaudisj  37889  bj-inftyexpidisj  37894  irrdiff  38010  relowlpssretop  38050  finxpreclem2  38076  finxpreclem3  38079  finxpreclem5  38081  nlpineqsn  38094  poimirlem18  38329  poimirlem19  38330  poimirlem20  38331  mblfinlem1  38348  suceldisj  39507  elpadd0  40623  pssn0  43038  oexpreposd  43123  diophin  43543  fiphp3d  43586  expdioph  43790  wepwsolem  43809  kelac1  43830  onov0suclim  44041  tfsconcatb0  44111  ensucne0  44295  relintabex  44347  brnonrel  44355  relexp01min  44479  iooinlbub  46257  stoweidlem34  46788  fourierdlem60  46920  fourierdlem61  46921  afv20defat  48009  minusmodnep2tmod  48136  spr0nelg  48265  sprsymrelfvlem  48279  fmtnoinf  48328  fmtno4prmfac193  48365  fmtno4prm  48367  31prm  48389  lighneallem3  48399  lighneallem4  48402  nnsum4primeseven  48605  nnsum4primesevenALTV  48606  dig2nn1st  49425  itcoval1  49483  line2ylem  49571  ipolub00  49811  fucofvalne  50143