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  4070  nel02  4302  n0i  4303  sbcel12  4374  sbcel2  4381  sbcbr123  5161  sbcbr  5162  axnul  5260  intex  5299  intnex  5300  iin0  5317  notzfaus  5318  nfcvb  5331  eunex  5345  opelopabsb  5490  brabv  5528  epelg  5539  0nelelxp  5673  elimasni  6062  onxpdisj  6460  ndmfvrcl  6894  canth  7341  fvmptopabOLD  7444  oprssdm  7570  ndmovrcl  7575  omelon2  7855  poxp2  8122  xpord2indlem  8126  poxp3  8129  undefnel2  8256  tfr2b  8364  tz7.44-3  8376  nlim2  8454  ord1eln01  8460  ord2eln012  8461  1ellim  8462  2ellim  8463  eceqoveq  8795  2dom  9001  omxpenlem  9042  domunsn  9091  disjen  9098  infensuc  9119  0sdom1dom  9185  1sdom2dom  9194  infn0  9251  elfi2  9365  en3lp  9567  preleqALT  9570  rankxpsuc  9835  updjudhcoinrg  9886  sdomsdomcardi  9924  cardmin2  9952  pm54.43lem  9953  pr2ne  9957  alephgeom  10035  alephval3  10063  cfsuc  10210  cflim2  10216  alephval2  10525  axunnd  10549  canthp1lem1  10605  pwxpndom2  10618  rankcf  10730  pinq  10880  adderpq  10909  mulerpq  10910  nqpr  10967  ltsopr  10985  ltapr  10998  renepnf  11222  renemnf  11223  lt0ne0d  11743  prodgt0  12029  nnne0ALT  12224  nn0nepnf  12523  xrltnr  13079  pnfnlt  13088  nltmnf  13089  xrltnsym  13097  nltpnft  13124  ngtmnft  13126  xsubge0  13221  xmullem2  13225  xlemul1a  13248  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  fzpreddisj  13534  fzm1  13568  uzinf  13930  hashnemnf  14309  hashclb  14323  hasheq0  14328  hashnn0n0nn  14356  prprrab  14438  tpf1ofv1  14462  tpf1ofv2  14463  lsw0  14530  cats1un  14686  geolim  15836  geolim2  15837  georeclim  15838  geoisumr  15844  m1exp1  16346  bitsfzolem  16404  bitsfzo  16405  bitsinv1lem  16411  sadcp1  16425  saddisjlem  16434  smu01lem  16455  3prm  16664  pcgcd1  16848  pc2dvds  16850  pcmpt  16863  prmreclem5  16891  vdwap0  16947  prmo1  17008  fvprif  17524  setcepi  18050  oduclatb  18466  smndex1n0mnd  18839  cntzrcl  19259  pmtrfrn  19388  pmtrprfval  19417  pmtrprfvalrn  19418  psgnunilem5  19424  odhash3  19506  gsumzaddlem  19851  gsumzsplit  19857  dprdcntz2  19970  trivnsimpgd  20029  0ringnnzr  20434  xrsdsreclblem  21329  dsmmfi  21647  islindf4  21747  mplcoe1  21944  mplcoe5  21947  psrbagsn  21970  pmatcollpw3fi1lem1  22673  istps  22821  haust1  23239  hauspwdom  23388  kqcldsat  23620  csdfil  23781  tsmssplit  24039  dscopn  24461  htpycc  24879  pco1  24915  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  itg11  25592  bddmulibl  25740  lhop1  25919  deg1nn0clb  25995  plypf1  26117  vieta1lem2  26219  logdmn0  26549  logcnlem3  26553  fsumharmonic  26922  sqff1o  27092  perfectlem1  27140  bposlem5  27199  lgsval2lem  27218  addsqrexnreu  27353  addsqnreup  27354  ostth  27550  sltval2  27568  sltintdifex  27573  sltres  27574  nolt02o  27607  nogt01o  27608  bday1s  27743  lrold  27808  lrrecpo  27848  mulsval  28012  legso  28526  axlowdimlem13  28881  axlowdimlem16  28884  axlowdim1  28886  axlowdim  28888  upgrfi  29018  lfgrnloop  29052  umgredgnlp  29074  wlkp1lem3  29603  rusgrnumwwlkl1  29898  clwwlk  29912  clwwlkn0  29957  clwwlknon1sn  30029  trlsegvdeg  30156  konigsberg  30186  ex-res  30370  norm1exi  31179  dmadjrnb  31835  strlem1  32179  largei  32196  ifeqeqx  32471  ubico  32698  expgt0b  32741  chnccats1  32941  0ringirng  33684  rtelextdg2lem  33716  2sqr3minply  33770  dya2iocuni  34274  eulerpartlemgh  34369  ballotlem4  34490  plymulx0  34538  signswch  34552  signstfvneq0  34563  signlem0  34578  subfacp1lem1  35166  fmlaomn0  35377  gonan0  35379  goaln0  35380  fmla0disjsuc  35385  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  prv1n  35418  bcneg1  35723  opelco3  35762  wsuclem  35813  dfrdg4  35939  linedegen  36131  rankeq1o  36159  hfninf  36174  ordcmp  36435  curryset  36934  currysetlem3  36937  bj-projval  36984  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  irrdiff  37314  relowlpssretop  37352  finxpreclem2  37378  finxpreclem3  37381  finxpreclem5  37383  nlpineqsn  37396  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  mblfinlem1  37651  elpadd0  39803  pssn0  42215  oexpreposd  42310  diophin  42760  fiphp3d  42807  expdioph  43012  wepwsolem  43031  kelac1  43052  onov0suclim  43263  tfsconcatb0  43333  ensucne0  43518  relintabex  43570  brnonrel  43578  relexp01min  43702  iooinlbub  45499  stoweidlem34  46032  fourierdlem60  46164  fourierdlem61  46165  tworepnotupword  46884  afv20defat  47233  minusmodnep2tmod  47354  spr0nelg  47477  sprsymrelfvlem  47491  fmtnoinf  47537  fmtno4prmfac193  47574  fmtno4prm  47576  31prm  47598  lighneallem3  47608  lighneallem4  47611  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  dig2nn1st  48594  itcoval1  48652  line2ylem  48740  ipolub00  48981  fucofvalne  49314