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  4056  nel02  4288  n0i  4289  sbcel12  4360  sbcel2  4367  sbcbr123  5147  sbcbr  5148  axnul  5245  intex  5284  intnex  5285  iin0  5302  notzfaus  5303  nfcvb  5316  eunex  5330  opelopabsb  5473  brabv  5509  epelg  5520  0nelelxp  5654  elimasni  6044  onxpdisj  6438  ndmfvrcl  6861  canth  7306  oprssdm  7533  ndmovrcl  7538  omelon2  7815  poxp2  8079  xpord2indlem  8083  poxp3  8086  undefnel2  8213  tfr2b  8321  tz7.44-3  8333  nlim2  8411  ord1eln01  8417  ord2eln012  8418  1ellim  8419  2ellim  8420  eceqoveq  8752  2dom  8959  omxpenlem  8998  domunsn  9047  disjen  9054  infensuc  9075  0sdom1dom  9137  1sdom2dom  9145  infn0  9193  elfi2  9305  en3lp  9511  preleqALT  9514  rankxpsuc  9782  updjudhcoinrg  9833  sdomsdomcardi  9871  cardmin2  9899  pm54.43lem  9900  pr2ne  9903  alephgeom  9980  alephval3  10008  cfsuc  10155  cflim2  10161  alephval2  10470  axunnd  10494  canthp1lem1  10550  pwxpndom2  10563  rankcf  10675  pinq  10825  adderpq  10854  mulerpq  10855  nqpr  10912  ltsopr  10930  ltapr  10943  renepnf  11167  renemnf  11168  lt0ne0d  11689  prodgt0  11975  nnne0ALT  12170  nn0nepnf  12469  xrltnr  13020  pnfnlt  13029  nltmnf  13030  xrltnsym  13038  nltpnft  13065  ngtmnft  13067  xsubge0  13162  xmullem2  13166  xlemul1a  13189  xrsupsslem  13208  xrinfmsslem  13209  xrub  13213  fzpreddisj  13475  fzm1  13509  uzinf  13874  hashnemnf  14253  hashclb  14267  hasheq0  14272  hashnn0n0nn  14300  prprrab  14382  tpf1ofv1  14406  tpf1ofv2  14407  lsw0  14474  cats1un  14630  geolim  15779  geolim2  15780  georeclim  15781  geoisumr  15787  m1exp1  16289  bitsfzolem  16347  bitsfzo  16348  bitsinv1lem  16354  sadcp1  16368  saddisjlem  16377  smu01lem  16398  3prm  16607  pcgcd1  16791  pc2dvds  16793  pcmpt  16806  prmreclem5  16834  vdwap0  16890  prmo1  16951  fvprif  17467  setcepi  17997  oduclatb  18415  chnccats1  18533  chnccat  18534  smndex1n0mnd  18822  cntzrcl  19241  pmtrfrn  19372  pmtrprfval  19401  pmtrprfvalrn  19402  psgnunilem5  19408  odhash3  19490  gsumzaddlem  19835  gsumzsplit  19841  dprdcntz2  19954  trivnsimpgd  20013  0ringnnzr  20442  xrsdsreclblem  21351  dsmmfi  21677  islindf4  21777  mplcoe1  21973  mplcoe5  21976  psrbagsn  21999  pmatcollpw3fi1lem1  22702  istps  22850  haust1  23268  hauspwdom  23417  kqcldsat  23649  csdfil  23810  tsmssplit  24068  dscopn  24489  htpycc  24907  pco1  24943  pcohtpylem  24947  pcopt  24950  pcopt2  24951  pcoass  24952  pcorevlem  24954  itg11  25620  bddmulibl  25768  lhop1  25947  deg1nn0clb  26023  plypf1  26145  vieta1lem2  26247  logdmn0  26577  logcnlem3  26581  fsumharmonic  26950  sqff1o  27120  perfectlem1  27168  bposlem5  27227  lgsval2lem  27246  addsqrexnreu  27381  addsqnreup  27382  ostth  27578  sltval2  27596  sltintdifex  27601  sltres  27602  nolt02o  27635  nogt01o  27636  bday1s  27776  lrold  27843  lrrecpo  27885  mulsval  28049  legso  28578  axlowdimlem13  28934  axlowdimlem16  28937  axlowdim1  28939  axlowdim  28941  upgrfi  29071  lfgrnloop  29105  umgredgnlp  29127  wlkp1lem3  29654  rusgrnumwwlkl1  29951  clwwlk  29965  clwwlkn0  30010  clwwlknon1sn  30082  trlsegvdeg  30209  konigsberg  30239  ex-res  30423  norm1exi  31232  dmadjrnb  31888  strlem1  32232  largei  32249  ifeqeqx  32524  ubico  32762  expgt0b  32804  0ringirng  33723  rtelextdg2lem  33760  2sqr3minply  33814  dya2iocuni  34317  eulerpartlemgh  34412  ballotlem4  34533  plymulx0  34581  signswch  34595  signstfvneq0  34606  signlem0  34621  subfacp1lem1  35244  fmlaomn0  35455  gonan0  35457  goaln0  35458  fmla0disjsuc  35463  ex-sategoelelomsuc  35491  ex-sategoelel12  35492  prv1n  35496  bcneg1  35801  opelco3  35840  wsuclem  35888  dfrdg4  36016  linedegen  36208  rankeq1o  36236  hfninf  36251  ordcmp  36512  curryset  37011  currysetlem3  37014  bj-projval  37061  bj-inftyexpitaudisj  37270  bj-inftyexpidisj  37275  irrdiff  37391  relowlpssretop  37429  finxpreclem2  37455  finxpreclem3  37458  finxpreclem5  37460  nlpineqsn  37473  poimirlem18  37698  poimirlem19  37699  poimirlem20  37700  mblfinlem1  37717  elpadd0  39928  pssn0  42345  oexpreposd  42440  diophin  42889  fiphp3d  42936  expdioph  43140  wepwsolem  43159  kelac1  43180  onov0suclim  43391  tfsconcatb0  43461  ensucne0  43646  relintabex  43698  brnonrel  43706  relexp01min  43830  iooinlbub  45625  stoweidlem34  46156  fourierdlem60  46288  fourierdlem61  46289  afv20defat  47356  minusmodnep2tmod  47477  spr0nelg  47600  sprsymrelfvlem  47614  fmtnoinf  47660  fmtno4prmfac193  47697  fmtno4prm  47699  31prm  47721  lighneallem3  47731  lighneallem4  47734  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  dig2nn1st  48730  itcoval1  48788  line2ylem  48876  ipolub00  49117  fucofvalne  49450