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  4048  nel02  4280  sbcel12  4352  sbcel2  4359  sbcbr123  5140  sbcbr  5141  axnul  5240  intex  5281  intnex  5282  iin0  5299  notzfaus  5300  nfcvb  5313  eunex  5327  opelopabsb  5478  brabv  5514  epelg  5525  0nelelxp  5659  elimasni  6050  onxpdisj  6444  ndmfvrcl  6867  canth  7314  oprssdm  7541  ndmovrcl  7546  omelon2  7823  poxp2  8086  xpord2indlem  8090  poxp3  8093  undefnel2  8220  tfr2b  8328  tz7.44-3  8340  nlim2  8418  ord1eln01  8424  ord2eln012  8425  1ellim  8426  2ellim  8427  eceqoveq  8762  2dom  8970  omxpenlem  9009  domunsn  9058  disjen  9065  infensuc  9086  ordfin  9143  0sdom1dom  9149  1sdom2dom  9157  infn0  9205  elfi2  9320  en3lp  9526  preleqALT  9529  rankxpsuc  9797  updjudhcoinrg  9848  sdomsdomcardi  9886  cardmin2  9914  pm54.43lem  9915  pr2ne  9918  alephgeom  9995  alephval3  10023  cfsuc  10170  cflim2  10176  alephval2  10486  axunnd  10510  canthp1lem1  10566  pwxpndom2  10579  rankcf  10691  pinq  10841  adderpq  10870  mulerpq  10871  nqpr  10928  ltsopr  10946  ltapr  10959  renepnf  11184  renemnf  11185  lt0ne0d  11706  prodgt0  11993  nnne0ALT  12206  nn0nepnf  12509  xrltnr  13061  pnfnlt  13070  nltmnf  13071  xrltnsym  13079  nltpnft  13107  ngtmnft  13109  xsubge0  13204  xmullem2  13208  xlemul1a  13231  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  fzpreddisj  13518  fzm1  13552  uzinf  13918  hashnemnf  14297  hashclb  14311  hasheq0  14316  hashnn0n0nn  14344  prprrab  14426  tpf1ofv1  14450  tpf1ofv2  14451  lsw0  14518  cats1un  14674  geolim  15826  geolim2  15827  georeclim  15828  geoisumr  15834  m1exp1  16336  bitsfzolem  16394  bitsfzo  16395  bitsinv1lem  16401  sadcp1  16415  saddisjlem  16424  smu01lem  16445  3prm  16654  pcgcd1  16839  pc2dvds  16841  pcmpt  16854  prmreclem5  16882  vdwap0  16938  prmo1  16999  fvprif  17516  setcepi  18046  oduclatb  18464  chnccats1  18582  chnccat  18583  smndex1n0mnd  18874  cntzrcl  19293  pmtrfrn  19424  pmtrprfval  19453  pmtrprfvalrn  19454  psgnunilem5  19460  odhash3  19542  gsumzaddlem  19887  gsumzsplit  19893  dprdcntz2  20006  trivnsimpgd  20065  0ringnnzr  20493  xrsdsreclblem  21402  dsmmfi  21728  islindf4  21828  mplcoe1  22025  mplcoe5  22028  psrbagsn  22051  pmatcollpw3fi1lem1  22761  istps  22909  haust1  23327  hauspwdom  23476  kqcldsat  23708  csdfil  23869  tsmssplit  24127  dscopn  24548  htpycc  24957  pco1  24992  pcohtpylem  24996  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  itg11  25668  bddmulibl  25816  lhop1  25991  deg1nn0clb  26065  plypf1  26187  vieta1lem2  26288  logdmn0  26617  logcnlem3  26621  fsumharmonic  26989  sqff1o  27159  perfectlem1  27206  bposlem5  27265  lgsval2lem  27284  addsqrexnreu  27419  addsqnreup  27420  ostth  27616  ltsval2  27634  ltsintdifex  27639  ltsres  27640  nolt02o  27673  nogt01o  27674  bday1  27820  lrold  27903  lrrecpo  27947  mulsval  28115  legso  28681  axlowdimlem13  29037  axlowdimlem16  29040  axlowdim1  29042  axlowdim  29044  upgrfi  29174  lfgrnloop  29208  umgredgnlp  29230  wlkp1lem3  29757  rusgrnumwwlkl1  30054  clwwlk  30068  clwwlkn0  30113  clwwlknon1sn  30185  trlsegvdeg  30312  konigsberg  30342  ex-res  30526  norm1exi  31336  dmadjrnb  31992  strlem1  32336  largei  32353  ifeqeqx  32627  ubico  32863  expgt0b  32905  0ringirng  33849  rtelextdg2lem  33886  2sqr3minply  33940  dya2iocuni  34443  eulerpartlemgh  34538  ballotlem4  34659  plymulx0  34707  signswch  34721  signstfvneq0  34732  signlem0  34747  xoromon  35248  fineqvomonb  35279  noinfepfnregs  35292  subfacp1lem1  35377  fmlaomn0  35588  gonan0  35590  goaln0  35591  fmla0disjsuc  35596  ex-sategoelelomsuc  35624  ex-sategoelel12  35625  prv1n  35629  bcneg1  35934  opelco3  35973  wsuclem  36021  dfrdg4  36149  linedegen  36341  rankeq1o  36369  hfninf  36384  ordcmp  36645  curryset  37269  currysetlem3  37272  bj-projval  37319  bj-inftyexpitaudisj  37535  bj-inftyexpidisj  37540  irrdiff  37656  relowlpssretop  37694  finxpreclem2  37720  finxpreclem3  37723  finxpreclem5  37725  nlpineqsn  37738  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  mblfinlem1  37992  suceldisj  39153  elpadd0  40269  pssn0  42682  oexpreposd  42768  diophin  43218  fiphp3d  43265  expdioph  43469  wepwsolem  43488  kelac1  43509  onov0suclim  43720  tfsconcatb0  43790  ensucne0  43974  relintabex  44026  brnonrel  44034  relexp01min  44158  iooinlbub  45949  stoweidlem34  46480  fourierdlem60  46612  fourierdlem61  46613  afv20defat  47692  minusmodnep2tmod  47819  spr0nelg  47948  sprsymrelfvlem  47962  fmtnoinf  48011  fmtno4prmfac193  48048  fmtno4prm  48050  31prm  48072  lighneallem3  48082  lighneallem4  48085  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  dig2nn1st  49093  itcoval1  49151  line2ylem  49239  ipolub00  49480  fucofvalne  49812