Theorem mtbiri 329

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 231	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtoi 201	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  psstr  4061  nel02  4291  sbcel12  4364  sbcel2  4371  sbcbr123  5153  sbcbr  5154  axnul  5254  intex  5299  intnex  5300  iin0  5318  notzfaus  5319  nfcvb  5332  eunex  5346  opelopabsb  5499  brabv  5535  epelg  5546  0nelelxp  5680  elimasni  6077  onxpdisj  6469  ndmfvrcl  6896  canth  7346  oprssdm  7573  ndmovrcl  7578  omelon2  7855  poxp2  8118  xpord2indlem  8122  poxp3  8125  undefnel2  8253  tfr2b  8362  tz7.44-3  8374  nlim2  8454  ord1eln01  8460  ord2eln012  8461  1ellim  8462  2ellim  8463  eceqoveq  8799  2dom  9007  omxpenlem  9046  domunsn  9095  disjen  9102  infensuc  9123  ordfin  9180  0sdom1dom  9186  1sdom2dom  9194  infn0  9242  elfi2  9357  en3lp  9566  preleqALT  9569  rankxpsuc  9837  updjudhcoinrg  9888  sdomsdomcardi  9926  cardmin2  9954  pm54.43lem  9955  pr2ne  9958  alephgeom  10035  alephval3  10063  cfsuc  10211  cflim2  10217  alephval2  10527  axunnd  10551  canthp1lem1  10607  pwxpndom2  10620  rankcf  10732  pinq  10882  adderpq  10911  mulerpq  10912  nqpr  10969  ltsopr  10987  ltapr  11000  renepnf  11227  renemnf  11228  lt0ne0d  11749  prodgt0  12035  nnne0ALT  12248  nn0nepnf  12559  xrltnr  13118  pnfnlt  13127  nltmnf  13128  xrltnsym  13136  nltpnft  13164  ngtmnft  13166  xsubge0  13261  xmullem2  13265  xlemul1a  13288  xrsupsslem  13307  xrinfmsslem  13308  xrub  13312  fzpreddisj  13575  fzm1  13609  uzinf  13975  hashnemnf  14354  hashclb  14368  hasheq0  14373  hashnn0n0nn  14401  prprrab  14483  tpf1ofv1  14507  tpf1ofv2  14508  lsw0  14575  cats1un  14731  geolim  15883  geolim2  15884  georeclim  15885  geoisumr  15891  m1exp1  16393  bitsfzolem  16451  bitsfzo  16452  bitsinv1lem  16458  sadcp1  16472  saddisjlem  16481  smu01lem  16502  3prm  16711  pcgcd1  16896  pc2dvds  16898  pcmpt  16911  prmreclem5  16939  vdwap0  16995  prmo1  17056  fvprif  17574  setcepi  18104  oduclatb  18522  chnccats1  18640  chnccat  18641  smndex1n0mnd  18932  cntzrcl  19350  pmtrfrn  19481  pmtrprfval  19510  pmtrprfvalrn  19511  psgnunilem5  19517  odhash3  19599  gsumzaddlem  19944  gsumzsplit  19950  dprdcntz2  20063  trivnsimpgd  20122  0ringnnzr  20554  xrsdsreclblem  21445  dsmmfi  21770  islindf4  21870  mplcoe1  22070  mplcoe5  22073  psrbagsn  22096  pmatcollpw3fi1lem1  22826  istps  22974  haust1  23392  hauspwdom  23541  kqcldsat  23773  csdfil  23934  tsmssplit  24192  dscopn  24613  htpycc  25022  pco1  25057  pcohtpylem  25061  pcopt  25064  pcopt2  25065  pcoass  25066  pcorevlem  25068  itg11  25733  bddmulibl  25881  lhop1  26056  deg1nn0clb  26130  plypf1  26252  vieta1lem2  26352  logdmn0  26682  logcnlem3  26686  fsumharmonic  27053  sqff1o  27223  perfectlem1  27270  bposlem5  27329  lgsval2lem  27348  addsqrexnreu  27483  addsqnreup  27484  ostth  27680  ltsval2  27697  ltsintdifex  27702  ltsres  27703  nolt02o  27736  nogt01o  27737  bday1  27884  lrold  27967  lrrecpo  28011  mulsval  28179  legso  28745  axlowdimlem13  29101  axlowdimlem16  29104  axlowdim1  29106  axlowdim  29108  upgrfi  29238  lfgrnloop  29272  umgredgnlp  29294  wlkp1lem3  29820  rusgrnumwwlkl1  30117  clwwlk  30131  clwwlkn0  30176  clwwlknon1sn  30248  trlsegvdeg  30375  konigsberg  30405  ex-res  30589  norm1exi  31399  dmadjrnb  32055  strlem1  32399  largei  32416  ifeqeqx  32690  ubico  32927  expgt0b  32969  0ringirng  33947  rtelextdg2lem  33984  2sqr3minply  34038  dya2iocuni  34541  eulerpartlemgh  34636  ballotlem4  34757  plymulx0  34805  signswch  34819  signstfvneq0  34830  signlem0  34845  xoromon  35348  fineqvomonb  35379  noinfepfnregs  35392  subfacp1lem1  35493  fmlaomn0  35704  gonan0  35706  goaln0  35707  fmla0disjsuc  35712  ex-sategoelelomsuc  35740  ex-sategoelel12  35741  prv1n  35745  bcneg1  36050  opelco3  36089  wsuclem  36137  dfrdg4  36265  linedegen  36457  rankeq1o  36485  hfninf  36500  ordcmp  36771  curryset  37395  currysetlem3  37398  bj-projval  37445  bj-inftyexpitaudisj  37661  bj-inftyexpidisj  37666  irrdiff  37782  relowlpssretop  37822  finxpreclem2  37848  finxpreclem3  37851  finxpreclem5  37853  nlpineqsn  37866  poimirlem18  38101  poimirlem19  38102  poimirlem20  38103  mblfinlem1  38120  suceldisj  39281  elpadd0  40397  pssn0  42810  oexpreposd  42895  diophin  43317  fiphp3d  43360  expdioph  43564  wepwsolem  43583  kelac1  43604  onov0suclim  43815  tfsconcatb0  43885  ensucne0  44069  relintabex  44121  brnonrel  44129  relexp01min  44253  iooinlbub  46041  stoweidlem34  46572  fourierdlem60  46704  fourierdlem61  46705  afv20defat  47790  minusmodnep2tmod  47917  spr0nelg  48046  sprsymrelfvlem  48060  fmtnoinf  48109  fmtno4prmfac193  48146  fmtno4prm  48148  31prm  48170  lighneallem3  48180  lighneallem4  48183  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  dig2nn1st  49191  itcoval1  49249  line2ylem  49337  ipolub00  49578  fucofvalne  49910