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  4116  nel02  4344  n0i  4345  sbcel12  4416  sbcel2  4423  sbcbr123  5201  sbcbr  5202  axnul  5310  intex  5349  intnex  5350  iin0  5367  notzfaus  5368  nfcvb  5381  eunex  5395  opelopabsb  5539  brabv  5577  epelg  5589  0nelelxp  5723  elimasni  6111  0ellim  6448  onxpdisj  6511  ndmfvrcl  6942  canth  7384  fvmptopabOLD  7487  oprssdm  7613  ndmovrcl  7618  omelon2  7899  poxp2  8166  xpord2indlem  8170  poxp3  8173  undefnel2  8300  tfr2b  8434  tz7.44-3  8446  nlim2  8526  ord1eln01  8532  ord2eln012  8533  1ellim  8534  2ellim  8535  eceqoveq  8860  2dom  9068  omxpenlem  9111  domunsn  9165  disjen  9172  infensuc  9193  snnen2oOLD  9261  0sdom1dom  9271  1sdom2dom  9280  infn0  9337  elfi2  9451  en3lp  9651  preleqALT  9654  rankxpsuc  9919  updjudhcoinrg  9970  sdomsdomcardi  10008  cardmin2  10036  pm54.43lem  10037  pr2ne  10041  alephgeom  10119  alephval3  10147  cfsuc  10294  cflim2  10300  alephval2  10609  axunnd  10633  canthp1lem1  10689  pwxpndom2  10702  rankcf  10814  pinq  10964  adderpq  10993  mulerpq  10994  nqpr  11051  ltsopr  11069  ltapr  11082  renepnf  11306  renemnf  11307  lt0ne0d  11825  prodgt0  12111  nnne0ALT  12301  nn0nepnf  12604  xrltnr  13158  pnfnlt  13167  nltmnf  13168  xrltnsym  13175  nltpnft  13202  ngtmnft  13204  xsubge0  13299  xmullem2  13303  xlemul1a  13326  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  fzpreddisj  13609  fzm1  13643  uzinf  14002  hashnemnf  14379  hashclb  14393  hasheq0  14398  hashnn0n0nn  14426  prprrab  14508  tpf1ofv1  14532  tpf1ofv2  14533  lsw0  14599  cats1un  14755  geolim  15902  geolim2  15903  georeclim  15904  geoisumr  15910  m1exp1  16409  bitsfzolem  16467  bitsfzo  16468  bitsinv1lem  16474  sadcp1  16488  saddisjlem  16497  smu01lem  16518  3prm  16727  pcgcd1  16910  pc2dvds  16912  pcmpt  16925  prmreclem5  16953  vdwap0  17009  prmo1  17070  fvprif  17607  setcepi  18141  oduclatb  18564  smndex1n0mnd  18937  cntzrcl  19357  pmtrfrn  19490  pmtrprfval  19519  pmtrprfvalrn  19520  psgnunilem5  19526  odhash3  19608  gsumzaddlem  19953  gsumzsplit  19959  dprdcntz2  20072  trivnsimpgd  20131  0ringnnzr  20541  xrsdsreclblem  21447  dsmmfi  21775  islindf4  21875  mplcoe1  22072  mplcoe5  22075  psrbagsn  22104  pmatcollpw3fi1lem1  22807  istps  22955  haust1  23375  hauspwdom  23524  kqcldsat  23756  csdfil  23917  tsmssplit  24175  dscopn  24601  htpycc  25025  pco1  25061  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  itg11  25739  bddmulibl  25888  lhop1  26067  deg1nn0clb  26143  plypf1  26265  vieta1lem2  26367  logdmn0  26696  logcnlem3  26700  fsumharmonic  27069  sqff1o  27239  perfectlem1  27287  bposlem5  27346  lgsval2lem  27365  addsqrexnreu  27500  addsqnreup  27501  ostth  27697  sltval2  27715  sltintdifex  27720  sltres  27721  nolt02o  27754  nogt01o  27755  bday1s  27890  lrold  27949  lrrecpo  27988  mulsval  28149  legso  28621  axlowdimlem13  28983  axlowdimlem16  28986  axlowdim1  28988  axlowdim  28990  upgrfi  29122  lfgrnloop  29156  umgredgnlp  29178  wlkp1lem3  29707  rusgrnumwwlkl1  29997  clwwlk  30011  clwwlkn0  30056  clwwlknon1sn  30128  trlsegvdeg  30255  konigsberg  30285  ex-res  30469  norm1exi  31278  dmadjrnb  31934  strlem1  32278  largei  32295  ifeqeqx  32562  ubico  32783  expgt0b  32822  0ringirng  33703  rtelextdg2lem  33731  2sqr3minply  33752  dya2iocuni  34264  eulerpartlemgh  34359  ballotlem4  34479  plymulx0  34540  signswch  34554  signstfvneq0  34565  signlem0  34580  subfacp1lem1  35163  fmlaomn0  35374  gonan0  35376  goaln0  35377  fmla0disjsuc  35382  ex-sategoelelomsuc  35410  ex-sategoelel12  35411  prv1n  35415  bcneg1  35715  opelco3  35755  wsuclem  35806  dfrdg4  35932  linedegen  36124  rankeq1o  36152  hfninf  36167  ordcmp  36429  curryset  36928  currysetlem3  36931  bj-projval  36978  bj-inftyexpitaudisj  37187  bj-inftyexpidisj  37192  irrdiff  37308  relowlpssretop  37346  finxpreclem2  37372  finxpreclem3  37375  finxpreclem5  37377  nlpineqsn  37390  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  mblfinlem1  37643  elpadd0  39791  pssn0  42244  oexpreposd  42335  diophin  42759  fiphp3d  42806  expdioph  43011  wepwsolem  43030  kelac1  43051  onov0suclim  43263  tfsconcatb0  43333  ensucne0  43518  relintabex  43570  brnonrel  43578  relexp01min  43702  iooinlbub  45453  stoweidlem34  45989  fourierdlem60  46121  fourierdlem61  46122  tworepnotupword  46839  afv20defat  47181  minusmodnep2tmod  47292  spr0nelg  47400  sprsymrelfvlem  47414  fmtnoinf  47460  fmtno4prmfac193  47497  fmtno4prm  47499  31prm  47521  lighneallem3  47531  lighneallem4  47534  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  dig2nn1st  48454  itcoval1  48512  line2ylem  48600  ipolub00  48781