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  4107  nel02  4339  n0i  4340  sbcel12  4411  sbcel2  4418  sbcbr123  5197  sbcbr  5198  axnul  5305  intex  5344  intnex  5345  iin0  5362  notzfaus  5363  nfcvb  5376  eunex  5390  opelopabsb  5535  brabv  5573  epelg  5585  0nelelxp  5720  elimasni  6109  0ellim  6447  onxpdisj  6510  ndmfvrcl  6942  canth  7385  fvmptopabOLD  7488  oprssdm  7614  ndmovrcl  7619  omelon2  7900  poxp2  8168  xpord2indlem  8172  poxp3  8175  undefnel2  8302  tfr2b  8436  tz7.44-3  8448  nlim2  8528  ord1eln01  8534  ord2eln012  8535  1ellim  8536  2ellim  8537  eceqoveq  8862  2dom  9070  omxpenlem  9113  domunsn  9167  disjen  9174  infensuc  9195  snnen2oOLD  9264  0sdom1dom  9274  1sdom2dom  9283  infn0  9340  elfi2  9454  en3lp  9654  preleqALT  9657  rankxpsuc  9922  updjudhcoinrg  9973  sdomsdomcardi  10011  cardmin2  10039  pm54.43lem  10040  pr2ne  10044  alephgeom  10122  alephval3  10150  cfsuc  10297  cflim2  10303  alephval2  10612  axunnd  10636  canthp1lem1  10692  pwxpndom2  10705  rankcf  10817  pinq  10967  adderpq  10996  mulerpq  10997  nqpr  11054  ltsopr  11072  ltapr  11085  renepnf  11309  renemnf  11310  lt0ne0d  11828  prodgt0  12114  nnne0ALT  12304  nn0nepnf  12607  xrltnr  13161  pnfnlt  13170  nltmnf  13171  xrltnsym  13179  nltpnft  13206  ngtmnft  13208  xsubge0  13303  xmullem2  13307  xlemul1a  13330  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  fzpreddisj  13613  fzm1  13647  uzinf  14006  hashnemnf  14383  hashclb  14397  hasheq0  14402  hashnn0n0nn  14430  prprrab  14512  tpf1ofv1  14536  tpf1ofv2  14537  lsw0  14603  cats1un  14759  geolim  15906  geolim2  15907  georeclim  15908  geoisumr  15914  m1exp1  16413  bitsfzolem  16471  bitsfzo  16472  bitsinv1lem  16478  sadcp1  16492  saddisjlem  16501  smu01lem  16522  3prm  16731  pcgcd1  16915  pc2dvds  16917  pcmpt  16930  prmreclem5  16958  vdwap0  17014  prmo1  17075  fvprif  17606  setcepi  18133  oduclatb  18552  smndex1n0mnd  18925  cntzrcl  19345  pmtrfrn  19476  pmtrprfval  19505  pmtrprfvalrn  19506  psgnunilem5  19512  odhash3  19594  gsumzaddlem  19939  gsumzsplit  19945  dprdcntz2  20058  trivnsimpgd  20117  0ringnnzr  20525  xrsdsreclblem  21430  dsmmfi  21758  islindf4  21858  mplcoe1  22055  mplcoe5  22058  psrbagsn  22087  pmatcollpw3fi1lem1  22792  istps  22940  haust1  23360  hauspwdom  23509  kqcldsat  23741  csdfil  23902  tsmssplit  24160  dscopn  24586  htpycc  25012  pco1  25048  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  itg11  25726  bddmulibl  25874  lhop1  26053  deg1nn0clb  26129  plypf1  26251  vieta1lem2  26353  logdmn0  26682  logcnlem3  26686  fsumharmonic  27055  sqff1o  27225  perfectlem1  27273  bposlem5  27332  lgsval2lem  27351  addsqrexnreu  27486  addsqnreup  27487  ostth  27683  sltval2  27701  sltintdifex  27706  sltres  27707  nolt02o  27740  nogt01o  27741  bday1s  27876  lrold  27935  lrrecpo  27974  mulsval  28135  legso  28607  axlowdimlem13  28969  axlowdimlem16  28972  axlowdim1  28974  axlowdim  28976  upgrfi  29108  lfgrnloop  29142  umgredgnlp  29164  wlkp1lem3  29693  rusgrnumwwlkl1  29988  clwwlk  30002  clwwlkn0  30047  clwwlknon1sn  30119  trlsegvdeg  30246  konigsberg  30276  ex-res  30460  norm1exi  31269  dmadjrnb  31925  strlem1  32269  largei  32286  ifeqeqx  32555  ubico  32777  expgt0b  32818  chnccats1  33005  0ringirng  33739  rtelextdg2lem  33767  2sqr3minply  33791  dya2iocuni  34285  eulerpartlemgh  34380  ballotlem4  34501  plymulx0  34562  signswch  34576  signstfvneq0  34587  signlem0  34602  subfacp1lem1  35184  fmlaomn0  35395  gonan0  35397  goaln0  35398  fmla0disjsuc  35403  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  prv1n  35436  bcneg1  35736  opelco3  35775  wsuclem  35826  dfrdg4  35952  linedegen  36144  rankeq1o  36172  hfninf  36187  ordcmp  36448  curryset  36947  currysetlem3  36950  bj-projval  36997  bj-inftyexpitaudisj  37206  bj-inftyexpidisj  37211  irrdiff  37327  relowlpssretop  37365  finxpreclem2  37391  finxpreclem3  37394  finxpreclem5  37396  nlpineqsn  37409  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  mblfinlem1  37664  elpadd0  39811  pssn0  42266  oexpreposd  42357  diophin  42783  fiphp3d  42830  expdioph  43035  wepwsolem  43054  kelac1  43075  onov0suclim  43287  tfsconcatb0  43357  ensucne0  43542  relintabex  43594  brnonrel  43602  relexp01min  43726  iooinlbub  45514  stoweidlem34  46049  fourierdlem60  46181  fourierdlem61  46182  tworepnotupword  46901  afv20defat  47244  minusmodnep2tmod  47355  spr0nelg  47463  sprsymrelfvlem  47477  fmtnoinf  47523  fmtno4prmfac193  47560  fmtno4prm  47562  31prm  47584  lighneallem3  47594  lighneallem4  47597  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  dig2nn1st  48526  itcoval1  48584  line2ylem  48672  ipolub00  48882  fucofvalne  49020