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  4057  nel02  4289  n0i  4290  sbcel12  4361  sbcel2  4368  sbcbr123  5145  sbcbr  5146  axnul  5243  intex  5282  intnex  5283  iin0  5300  notzfaus  5301  nfcvb  5314  eunex  5328  opelopabsb  5470  brabv  5506  epelg  5517  0nelelxp  5651  elimasni  6040  onxpdisj  6433  ndmfvrcl  6855  canth  7300  oprssdm  7527  ndmovrcl  7532  omelon2  7809  poxp2  8073  xpord2indlem  8077  poxp3  8080  undefnel2  8207  tfr2b  8315  tz7.44-3  8327  nlim2  8405  ord1eln01  8411  ord2eln012  8412  1ellim  8413  2ellim  8414  eceqoveq  8746  2dom  8952  omxpenlem  8991  domunsn  9040  disjen  9047  infensuc  9068  0sdom1dom  9130  1sdom2dom  9138  infn0  9186  elfi2  9298  en3lp  9504  preleqALT  9507  rankxpsuc  9772  updjudhcoinrg  9823  sdomsdomcardi  9861  cardmin2  9889  pm54.43lem  9890  pr2ne  9893  alephgeom  9970  alephval3  9998  cfsuc  10145  cflim2  10151  alephval2  10460  axunnd  10484  canthp1lem1  10540  pwxpndom2  10553  rankcf  10665  pinq  10815  adderpq  10844  mulerpq  10845  nqpr  10902  ltsopr  10920  ltapr  10933  renepnf  11157  renemnf  11158  lt0ne0d  11679  prodgt0  11965  nnne0ALT  12160  nn0nepnf  12459  xrltnr  13015  pnfnlt  13024  nltmnf  13025  xrltnsym  13033  nltpnft  13060  ngtmnft  13062  xsubge0  13157  xmullem2  13161  xlemul1a  13184  xrsupsslem  13203  xrinfmsslem  13204  xrub  13208  fzpreddisj  13470  fzm1  13504  uzinf  13869  hashnemnf  14248  hashclb  14262  hasheq0  14267  hashnn0n0nn  14295  prprrab  14377  tpf1ofv1  14401  tpf1ofv2  14402  lsw0  14469  cats1un  14625  geolim  15774  geolim2  15775  georeclim  15776  geoisumr  15782  m1exp1  16284  bitsfzolem  16342  bitsfzo  16343  bitsinv1lem  16349  sadcp1  16363  saddisjlem  16372  smu01lem  16393  3prm  16602  pcgcd1  16786  pc2dvds  16788  pcmpt  16801  prmreclem5  16829  vdwap0  16885  prmo1  16946  fvprif  17462  setcepi  17992  oduclatb  18410  chnccats1  18528  chnccat  18529  smndex1n0mnd  18817  cntzrcl  19237  pmtrfrn  19368  pmtrprfval  19397  pmtrprfvalrn  19398  psgnunilem5  19404  odhash3  19486  gsumzaddlem  19831  gsumzsplit  19837  dprdcntz2  19950  trivnsimpgd  20009  0ringnnzr  20438  xrsdsreclblem  21347  dsmmfi  21673  islindf4  21773  mplcoe1  21970  mplcoe5  21973  psrbagsn  21996  pmatcollpw3fi1lem1  22699  istps  22847  haust1  23265  hauspwdom  23414  kqcldsat  23646  csdfil  23807  tsmssplit  24065  dscopn  24486  htpycc  24904  pco1  24940  pcohtpylem  24944  pcopt  24947  pcopt2  24948  pcoass  24949  pcorevlem  24951  itg11  25617  bddmulibl  25765  lhop1  25944  deg1nn0clb  26020  plypf1  26142  vieta1lem2  26244  logdmn0  26574  logcnlem3  26578  fsumharmonic  26947  sqff1o  27117  perfectlem1  27165  bposlem5  27224  lgsval2lem  27243  addsqrexnreu  27378  addsqnreup  27379  ostth  27575  sltval2  27593  sltintdifex  27598  sltres  27599  nolt02o  27632  nogt01o  27633  bday1s  27773  lrold  27840  lrrecpo  27882  mulsval  28046  legso  28575  axlowdimlem13  28930  axlowdimlem16  28933  axlowdim1  28935  axlowdim  28937  upgrfi  29067  lfgrnloop  29101  umgredgnlp  29123  wlkp1lem3  29650  rusgrnumwwlkl1  29944  clwwlk  29958  clwwlkn0  30003  clwwlknon1sn  30075  trlsegvdeg  30202  konigsberg  30232  ex-res  30416  norm1exi  31225  dmadjrnb  31881  strlem1  32225  largei  32242  ifeqeqx  32517  ubico  32753  expgt0b  32794  0ringirng  33697  rtelextdg2lem  33734  2sqr3minply  33788  dya2iocuni  34291  eulerpartlemgh  34386  ballotlem4  34507  plymulx0  34555  signswch  34569  signstfvneq0  34580  signlem0  34595  subfacp1lem1  35211  fmlaomn0  35422  gonan0  35424  goaln0  35425  fmla0disjsuc  35430  ex-sategoelelomsuc  35458  ex-sategoelel12  35459  prv1n  35463  bcneg1  35768  opelco3  35807  wsuclem  35858  dfrdg4  35984  linedegen  36176  rankeq1o  36204  hfninf  36219  ordcmp  36480  curryset  36979  currysetlem3  36982  bj-projval  37029  bj-inftyexpitaudisj  37238  bj-inftyexpidisj  37243  irrdiff  37359  relowlpssretop  37397  finxpreclem2  37423  finxpreclem3  37426  finxpreclem5  37428  nlpineqsn  37441  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  mblfinlem1  37696  elpadd0  39847  pssn0  42259  oexpreposd  42354  diophin  42804  fiphp3d  42851  expdioph  43055  wepwsolem  43074  kelac1  43095  onov0suclim  43306  tfsconcatb0  43376  ensucne0  43561  relintabex  43613  brnonrel  43621  relexp01min  43745  iooinlbub  45540  stoweidlem34  46071  fourierdlem60  46203  fourierdlem61  46204  afv20defat  47262  minusmodnep2tmod  47383  spr0nelg  47506  sprsymrelfvlem  47520  fmtnoinf  47566  fmtno4prmfac193  47603  fmtno4prm  47605  31prm  47627  lighneallem3  47637  lighneallem4  47640  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  dig2nn1st  48636  itcoval1  48694  line2ylem  48782  ipolub00  49023  fucofvalne  49356