Theorem mtbiri 330

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  psstr  4056  nel02  4285  sbcel12  4369  sbcel2  4376  sbcbr123  5159  sbcbr  5160  axnul  5259  intex  5305  intnex  5306  iin0  5324  notsep  5325  nfcvb  5338  eunex  5352  opelopabsb  5504  brabv  5541  epelg  5552  0nelelxp  5686  elimasni  6085  onxpdisj  6483  ndmfvrcl  6910  canth  7366  oprssdm  7594  ndmovrcl  7599  omelon2  7879  poxp2  8144  xpord2indlem  8148  poxp3  8151  undefnel2  8279  tfr2b  8388  tz7.44-3  8400  nlim2  8482  ord1eln01  8488  ord2eln012  8489  1ellim  8490  2ellim  8491  eceqoveq  8827  2dom  9042  omxpenlem  9081  domunsn  9130  disjen  9137  infensuc  9158  ordfin  9215  0sdom1dom  9221  1sdom2dom  9229  infn0  9278  elfi2  9390  en3lp  9599  preleqALT  9602  rankxpsuc  9880  updjudhcoinrg  9995  sdomsdomcardi  10033  cardmin2  10061  pm54.43lem  10062  pr2ne  10065  alephgeom  10142  alephval3  10170  cfsuc  10316  cflim2  10322  alephval2  10638  axunnd  10662  canthp1lem1  10718  pwxpndom2  10731  rankcf  10843  pinq  10993  adderpq  11022  mulerpq  11023  nqpr  11080  ltsopr  11098  ltapr  11111  renepnf  11338  renemnf  11339  lt0ne0d  11862  prodgt0  12145  nnne0ALT  12357  nn0nepnf  12668  xrltnr  13229  pnfnlt  13238  nltmnf  13239  xrltnsym  13247  nltpnft  13275  ngtmnft  13277  xsubge0  13372  xmullem2  13376  xlemul1a  13399  xrsupsslem  13418  xrinfmsslem  13419  xrub  13423  fzpreddisj  13687  fzm1  13721  uzinf  14088  hashnemnf  14468  hashclb  14482  hasheq0  14487  hashnn0n0nn  14515  prprrab  14598  tpf1ofv1  14622  tpf1ofv2  14623  lsw0  14690  cats1un  14850  geolim  16019  geolim2  16020  georeclim  16021  geoisumr  16027  m1exp1  16526  bitsfzolem  16584  bitsfzo  16585  bitsinv1lem  16591  sadcp1  16605  saddisjlem  16614  smu01lem  16635  3prm  16849  pcgcd1  17035  pc2dvds  17037  pcmpt  17050  prmreclem5  17078  vdwap0  17134  prmo1  17195  fvprif  17713  setcepi  18243  oduclatb  18661  chnccats1  18779  chnccat  18780  smndex1n0mnd  19091  cntzrcl  19521  pmtrfrn  19652  pmtrprfval  19681  pmtrprfvalrn  19682  psgnunilem5  19688  odhash3  19770  gsumzaddlem  20115  gsumzsplit  20121  dprdcntz2  20234  trivnsimpgd  20293  0ringnnzr  20756  xrsdsreclblem  21699  dsmmfi  22024  islindf4  22124  mplcoe1  22326  mplcoe5  22329  psrbagsn  22352  pmatcollpw3fi1lem1  23084  istps  23232  haust1  23650  hauspwdom  23800  kqcldsat  24032  csdfil  24193  tsmssplit  24451  dscopn  24872  htpycc  25281  pco1  25316  pcohtpylem  25320  pcopt  25323  pcopt2  25324  pcoass  25325  pcorevlem  25327  itg11  25992  bddmulibl  26139  lhop1  26314  deg1nn0clb  26388  plypf1  26511  plyn0mulidp  26584  vieta1lem2  26616  logdmn0  26950  logcnlem3  26954  fsumharmonic  27321  sqff1o  27491  perfectlem1  27538  bposlem5  27597  lgsval2lem  27616  addsqrexnreu  27751  addsqnreup  27752  ostth  27948  ltsval2  27995  ltsintdifex  28000  ltsres  28001  nolt02o  28034  nogt01o  28035  bday1  28182  lrold  28265  lrrecpo  28309  mulsval  28477  legso  29044  axlowdimlem13  29514  axlowdimlem16  29517  axlowdim1  29519  axlowdim  29521  upgrfi  29651  lfgrnloop  29685  umgredgnlp  29707  wlkp1lem3  30236  rusgrnumwwlkl1  30542  clwwlk  30556  clwwlkn0  30601  clwwlknon1sn  30673  trlsegvdeg  30810  konigsberg  30840  ex-res  31024  norm1exi  31834  dmadjrnb  32490  strlem1  32834  largei  32851  ifeqeqx  33120  ubico  33349  expgt0b  33390  0ringirng  34303  rtelextdg2lem  34340  2sqr3minply  34394  dya2iocuni  34898  eulerpartlemgh  34993  ballotlem4  35114  signswch  35173  signstfvneq0  35184  signlem0  35199  xoromon  35697  fineqvomonb  35760  noinfepfnregs  35773  subfacp1lem1  35913  fmlaomn0  36124  gonan0  36126  goaln0  36127  fmla0disjsuc  36132  ex-sategoelelomsuc  36160  ex-sategoelel12  36161  prv1n  36165  bcneg1  36470  opelco3  36509  wsuclem  36557  dfrdg4  36685  linedegen  36878  rankeq1o  36902  hfninf  36905  ordcmp  37205  curryset  37829  currysetlem3  37832  bj-projval  37879  bj-inftyexpitaudisj  38094  bj-inftyexpidisj  38099  irrdiff  38215  relowlpssretop  38255  finxpreclem2  38281  finxpreclem3  38284  finxpreclem5  38286  nlpineqsn  38299  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  mblfinlem1  38543  suceldisj  39718  elpadd0  40834  pssn0  43249  oexpreposd  43347  diophin  43736  fiphp3d  43779  expdioph  43983  wepwsolem  44002  kelac1  44023  onov0suclim  44234  tfsconcatb0  44304  ensucne0  44488  relintabex  44540  brnonrel  44548  relexp01min  44672  iooinlbub  46457  stoweidlem34  46988  fourierdlem60  47120  fourierdlem61  47121  afv20defat  48246  minusmodnep2tmod  48373  spr0nelg  48502  sprsymrelfvlem  48516  fmtnoinf  48565  fmtno4prmfac193  48602  fmtno4prm  48604  31prm  48626  lighneallem3  48636  lighneallem4  48639  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  dig2nn1st  49661  itcoval1  49719  line2ylem  49807  ipolub00  50045  fucofvalne  50377