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  4130  nel02  4362  n0i  4363  sbcel12  4434  sbcel2  4441  sbcbr123  5220  sbcbr  5221  axnul  5323  intex  5362  intnex  5363  iin0  5380  notzfaus  5381  nfcvb  5394  eunex  5408  opelopabsb  5549  brabv  5588  epelg  5600  0nelelxp  5735  elimasni  6121  0ellim  6458  onxpdisj  6521  ndmfvrcl  6956  canth  7401  fvmptopabOLD  7505  oprssdm  7631  ndmovrcl  7636  omelon2  7916  poxp2  8184  xpord2indlem  8188  poxp3  8191  undefnel2  8318  tfr2b  8452  tz7.44-3  8464  nlim2  8546  ord1eln01  8552  ord2eln012  8553  1ellim  8554  2ellim  8555  eceqoveq  8880  2dom  9095  omxpenlem  9139  domunsn  9193  disjen  9200  infensuc  9221  snnen2oOLD  9290  0sdom1dom  9301  1sdom2dom  9310  infn0  9368  elfi2  9483  en3lp  9683  preleqALT  9686  rankxpsuc  9951  updjudhcoinrg  10002  sdomsdomcardi  10040  cardmin2  10068  pm54.43lem  10069  pr2ne  10073  alephgeom  10151  alephval3  10179  cfsuc  10326  cflim2  10332  alephval2  10641  axunnd  10665  canthp1lem1  10721  pwxpndom2  10734  rankcf  10846  pinq  10996  adderpq  11025  mulerpq  11026  nqpr  11083  ltsopr  11101  ltapr  11114  renepnf  11338  renemnf  11339  lt0ne0d  11855  prodgt0  12141  nnne0ALT  12331  nn0nepnf  12633  xrltnr  13182  pnfnlt  13191  nltmnf  13192  xrltnsym  13199  nltpnft  13226  ngtmnft  13228  xsubge0  13323  xmullem2  13327  xlemul1a  13350  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  fzpreddisj  13633  fzm1  13664  uzinf  14016  hashnemnf  14393  hashclb  14407  hasheq0  14412  hashnn0n0nn  14440  prprrab  14522  tpf1ofv1  14546  tpf1ofv2  14547  lsw0  14613  cats1un  14769  geolim  15918  geolim2  15919  georeclim  15920  geoisumr  15926  m1exp1  16424  bitsfzolem  16480  bitsfzo  16481  bitsinv1lem  16487  sadcp1  16501  saddisjlem  16510  smu01lem  16531  3prm  16741  pcgcd1  16924  pc2dvds  16926  pcmpt  16939  prmreclem5  16967  vdwap0  17023  prmo1  17084  fvprif  17621  setcepi  18155  oduclatb  18577  smndex1n0mnd  18947  cntzrcl  19367  pmtrfrn  19500  pmtrprfval  19529  pmtrprfvalrn  19530  psgnunilem5  19536  odhash3  19618  gsumzaddlem  19963  gsumzsplit  19969  dprdcntz2  20082  trivnsimpgd  20141  0ringnnzr  20551  xrsdsreclblem  21453  dsmmfi  21781  islindf4  21881  mplcoe1  22078  mplcoe5  22081  psrbagsn  22110  pmatcollpw3fi1lem1  22813  istps  22961  haust1  23381  hauspwdom  23530  kqcldsat  23762  csdfil  23923  tsmssplit  24181  dscopn  24607  htpycc  25031  pco1  25067  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  itg11  25745  bddmulibl  25894  lhop1  26073  deg1nn0clb  26149  plypf1  26271  vieta1lem2  26371  logdmn0  26700  logcnlem3  26704  fsumharmonic  27073  sqff1o  27243  perfectlem1  27291  bposlem5  27350  lgsval2lem  27369  addsqrexnreu  27504  addsqnreup  27505  ostth  27701  sltval2  27719  sltintdifex  27724  sltres  27725  nolt02o  27758  nogt01o  27759  bday1s  27894  lrold  27953  lrrecpo  27992  mulsval  28153  legso  28625  axlowdimlem13  28987  axlowdimlem16  28990  axlowdim1  28992  axlowdim  28994  upgrfi  29126  lfgrnloop  29160  umgredgnlp  29182  wlkp1lem3  29711  rusgrnumwwlkl1  30001  clwwlk  30015  clwwlkn0  30060  clwwlknon1sn  30132  trlsegvdeg  30259  konigsberg  30289  ex-res  30473  norm1exi  31282  dmadjrnb  31938  strlem1  32282  largei  32299  ifeqeqx  32565  ubico  32780  expgt0b  32820  0ringirng  33689  rtelextdg2lem  33717  2sqr3minply  33738  dya2iocuni  34248  eulerpartlemgh  34343  ballotlem4  34463  plymulx0  34524  signswch  34538  signstfvneq0  34549  signlem0  34564  subfacp1lem1  35147  fmlaomn0  35358  gonan0  35360  goaln0  35361  fmla0disjsuc  35366  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv1n  35399  bcneg1  35698  opelco3  35738  wsuclem  35789  dfrdg4  35915  linedegen  36107  rankeq1o  36135  hfninf  36150  ordcmp  36413  curryset  36912  currysetlem3  36915  bj-projval  36962  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  irrdiff  37292  relowlpssretop  37330  finxpreclem2  37356  finxpreclem3  37359  finxpreclem5  37361  nlpineqsn  37374  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  mblfinlem1  37617  elpadd0  39766  pssn0  42220  oexpreposd  42309  diophin  42728  fiphp3d  42775  expdioph  42980  wepwsolem  42999  kelac1  43020  onov0suclim  43236  tfsconcatb0  43306  ensucne0  43491  relintabex  43543  brnonrel  43551  relexp01min  43675  iooinlbub  45419  stoweidlem34  45955  fourierdlem60  46087  fourierdlem61  46088  tworepnotupword  46805  afv20defat  47147  spr0nelg  47350  sprsymrelfvlem  47364  fmtnoinf  47410  fmtno4prmfac193  47447  fmtno4prm  47449  31prm  47471  lighneallem3  47481  lighneallem4  47484  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  dig2nn1st  48339  itcoval1  48397  line2ylem  48485  ipolub00  48665