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  4061  nel02  4293  n0i  4294  sbcel12  4365  sbcel2  4372  sbcbr123  5154  sbcbr  5155  axnul  5252  intex  5291  intnex  5292  iin0  5309  notzfaus  5310  nfcvb  5323  eunex  5337  opelopabsb  5486  brabv  5522  epelg  5533  0nelelxp  5667  elimasni  6058  onxpdisj  6452  ndmfvrcl  6875  canth  7322  oprssdm  7549  ndmovrcl  7554  omelon2  7831  poxp2  8095  xpord2indlem  8099  poxp3  8102  undefnel2  8229  tfr2b  8337  tz7.44-3  8349  nlim2  8427  ord1eln01  8433  ord2eln012  8434  1ellim  8435  2ellim  8436  eceqoveq  8771  2dom  8979  omxpenlem  9018  domunsn  9067  disjen  9074  infensuc  9095  ordfin  9152  0sdom1dom  9158  1sdom2dom  9166  infn0  9214  elfi2  9329  en3lp  9535  preleqALT  9538  rankxpsuc  9806  updjudhcoinrg  9857  sdomsdomcardi  9895  cardmin2  9923  pm54.43lem  9924  pr2ne  9927  alephgeom  10004  alephval3  10032  cfsuc  10179  cflim2  10185  alephval2  10495  axunnd  10519  canthp1lem1  10575  pwxpndom2  10588  rankcf  10700  pinq  10850  adderpq  10879  mulerpq  10880  nqpr  10937  ltsopr  10955  ltapr  10968  renepnf  11192  renemnf  11193  lt0ne0d  11714  prodgt0  12000  nnne0ALT  12195  nn0nepnf  12494  xrltnr  13045  pnfnlt  13054  nltmnf  13055  xrltnsym  13063  nltpnft  13091  ngtmnft  13093  xsubge0  13188  xmullem2  13192  xlemul1a  13215  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  fzpreddisj  13501  fzm1  13535  uzinf  13900  hashnemnf  14279  hashclb  14293  hasheq0  14298  hashnn0n0nn  14326  prprrab  14408  tpf1ofv1  14432  tpf1ofv2  14433  lsw0  14500  cats1un  14656  geolim  15805  geolim2  15806  georeclim  15807  geoisumr  15813  m1exp1  16315  bitsfzolem  16373  bitsfzo  16374  bitsinv1lem  16380  sadcp1  16394  saddisjlem  16403  smu01lem  16424  3prm  16633  pcgcd1  16817  pc2dvds  16819  pcmpt  16832  prmreclem5  16860  vdwap0  16916  prmo1  16977  fvprif  17494  setcepi  18024  oduclatb  18442  chnccats1  18560  chnccat  18561  smndex1n0mnd  18849  cntzrcl  19268  pmtrfrn  19399  pmtrprfval  19428  pmtrprfvalrn  19429  psgnunilem5  19435  odhash3  19517  gsumzaddlem  19862  gsumzsplit  19868  dprdcntz2  19981  trivnsimpgd  20040  0ringnnzr  20470  xrsdsreclblem  21379  dsmmfi  21705  islindf4  21805  mplcoe1  22004  mplcoe5  22007  psrbagsn  22030  pmatcollpw3fi1lem1  22742  istps  22890  haust1  23308  hauspwdom  23457  kqcldsat  23689  csdfil  23850  tsmssplit  24108  dscopn  24529  htpycc  24947  pco1  24983  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  itg11  25660  bddmulibl  25808  lhop1  25987  deg1nn0clb  26063  plypf1  26185  vieta1lem2  26287  logdmn0  26617  logcnlem3  26621  fsumharmonic  26990  sqff1o  27160  perfectlem1  27208  bposlem5  27267  lgsval2lem  27286  addsqrexnreu  27421  addsqnreup  27422  ostth  27618  ltsval2  27636  ltsintdifex  27641  ltsres  27642  nolt02o  27675  nogt01o  27676  bday1  27822  lrold  27905  lrrecpo  27949  mulsval  28117  legso  28683  axlowdimlem13  29039  axlowdimlem16  29042  axlowdim1  29044  axlowdim  29046  upgrfi  29176  lfgrnloop  29210  umgredgnlp  29232  wlkp1lem3  29759  rusgrnumwwlkl1  30056  clwwlk  30070  clwwlkn0  30115  clwwlknon1sn  30187  trlsegvdeg  30314  konigsberg  30344  ex-res  30528  norm1exi  31337  dmadjrnb  31993  strlem1  32337  largei  32354  ifeqeqx  32628  ubico  32865  expgt0b  32907  0ringirng  33866  rtelextdg2lem  33903  2sqr3minply  33957  dya2iocuni  34460  eulerpartlemgh  34555  ballotlem4  34676  plymulx0  34724  signswch  34738  signstfvneq0  34749  signlem0  34764  xoromon  35264  fineqvomonb  35294  noinfepfnregs  35307  subfacp1lem1  35392  fmlaomn0  35603  gonan0  35605  goaln0  35606  fmla0disjsuc  35611  ex-sategoelelomsuc  35639  ex-sategoelel12  35640  prv1n  35644  bcneg1  35949  opelco3  35988  wsuclem  36036  dfrdg4  36164  linedegen  36356  rankeq1o  36384  hfninf  36399  ordcmp  36660  curryset  37188  currysetlem3  37191  bj-projval  37238  bj-inftyexpitaudisj  37454  bj-inftyexpidisj  37459  irrdiff  37575  relowlpssretop  37613  finxpreclem2  37639  finxpreclem3  37642  finxpreclem5  37644  nlpineqsn  37657  poimirlem18  37883  poimirlem19  37884  poimirlem20  37885  mblfinlem1  37902  suceldisj  39063  elpadd0  40179  pssn0  42593  oexpreposd  42686  diophin  43123  fiphp3d  43170  expdioph  43374  wepwsolem  43393  kelac1  43414  onov0suclim  43625  tfsconcatb0  43695  ensucne0  43879  relintabex  43931  brnonrel  43939  relexp01min  44063  iooinlbub  45855  stoweidlem34  46386  fourierdlem60  46518  fourierdlem61  46519  afv20defat  47586  minusmodnep2tmod  47707  spr0nelg  47830  sprsymrelfvlem  47844  fmtnoinf  47890  fmtno4prmfac193  47927  fmtno4prm  47929  31prm  47951  lighneallem3  47961  lighneallem4  47964  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  dig2nn1st  48959  itcoval1  49017  line2ylem  49105  ipolub00  49346  fucofvalne  49678