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  4035  nel02  4284  sbcel12  4368  sbcel2  4375  sbcbr123  5159  sbcbr  5160  axnul  5258  intex  5304  intnex  5305  iin0  5323  notsep  5324  nfcvb  5337  eunex  5351  opelopabsb  5503  brabv  5540  epelg  5551  0nelelxp  5685  elimasni  6088  onxpdisj  6490  ndmfvrcl  6918  canth  7374  oprssdm  7602  ndmovrcl  7607  omelon2  7890  poxp2  8162  xpord2indlem  8166  poxp3  8169  undefnel2  8298  tfr2b  8407  tz7.44-3  8419  nlim2  8501  ord1eln01  8507  ord2eln012  8508  1ellim  8509  2ellim  8510  eceqoveq  8846  2dom  9061  omxpenlem  9100  domunsn  9149  disjen  9156  infensuc  9177  ordfin  9234  0sdom1dom  9240  1sdom2dom  9248  infn0  9297  elfi2  9409  en3lp  9618  preleqALT  9621  rankxpsuc  9902  updjudhcoinrg  10017  sdomsdomcardi  10055  cardmin2  10083  pm54.43lem  10084  pr2ne  10087  alephgeom  10164  alephval3  10192  cfsuc  10338  cflim2  10344  alephval2  10660  axunnd  10684  canthp1lem1  10740  pwxpndom2  10753  rankcf  10865  pinq  11015  adderpq  11044  mulerpq  11045  nqpr  11102  ltsopr  11120  ltapr  11133  renepnf  11360  renemnf  11361  lt0ne0d  11884  prodgt0  12167  nnne0ALT  12379  nn0nepnf  12690  xrltnr  13251  pnfnlt  13260  nltmnf  13261  xrltnsym  13269  nltpnft  13297  ngtmnft  13299  xsubge0  13394  xmullem2  13398  xlemul1a  13421  xrsupsslem  13440  xrinfmsslem  13441  xrub  13445  fzpreddisj  13710  fzm1  13744  uzinf  14111  hashnemnf  14491  hashclb  14505  hasheq0  14510  hashnn0n0nn  14538  prprrab  14621  tpf1ofv1  14645  tpf1ofv2  14646  lsw0  14713  cats1un  14874  geolim  16044  geolim2  16045  georeclim  16046  geoisumr  16052  m1exp1  16551  bitsfzolem  16609  bitsfzo  16610  bitsinv1lem  16616  sadcp1  16630  saddisjlem  16639  smu01lem  16660  3prm  16874  pcgcd1  17060  pc2dvds  17062  pcmpt  17075  prmreclem5  17103  vdwap0  17159  prmo1  17220  fvprif  17738  setcepi  18268  oduclatb  18686  chnccats1  18804  chnccat  18805  smndex1n0mnd  19116  cntzrcl  19546  pmtrfrn  19677  pmtrprfval  19706  pmtrprfvalrn  19707  psgnunilem5  19713  odhash3  19795  gsumzaddlem  20140  gsumzsplit  20146  dprdcntz2  20259  trivnsimpgd  20318  0ringnnzr  20781  xrsdsreclblem  21724  dsmmfi  22049  islindf4  22149  mplcoe1  22351  mplcoe5  22354  psrbagsn  22377  pmatcollpw3fi1lem1  23109  istps  23257  haust1  23675  hauspwdom  23825  kqcldsat  24057  csdfil  24218  tsmssplit  24476  dscopn  24897  htpycc  25306  pco1  25341  pcohtpylem  25345  pcopt  25348  pcopt2  25349  pcoass  25350  pcorevlem  25352  itg11  26017  bddmulibl  26164  lhop1  26339  deg1nn0clb  26413  plypf1  26536  plyn0mulidp  26607  vieta1lem2  26639  logdmn0  26973  logcnlem3  26977  fsumharmonic  27344  sqff1o  27514  perfectlem1  27561  bposlem5  27620  lgsval2lem  27639  addsqrexnreu  27774  addsqnreup  27775  ostth  27971  ltsval2  28018  ltsintdifex  28023  ltsres  28024  nolt02o  28057  nogt01o  28058  bday1  28205  lrold  28288  lrrecpo  28332  mulsval  28500  legso  29067  axlowdimlem13  29537  axlowdimlem16  29540  axlowdim1  29542  axlowdim  29544  upgrfi  29674  lfgrnloop  29708  umgredgnlp  29730  wlkp1lem3  30259  rusgrnumwwlkl1  30565  clwwlk  30579  clwwlkn0  30624  clwwlknon1sn  30696  trlsegvdeg  30833  konigsberg  30863  ex-res  31047  norm1exi  31857  dmadjrnb  32513  strlem1  32857  largei  32874  ifeqeqx  33185  ubico  33413  expgt0b  33454  0ringirng  34367  rtelextdg2lem  34404  2sqr3minply  34458  dya2iocuni  34961  eulerpartlemgh  35056  ballotlem4  35177  signswch  35236  signstfvneq0  35247  signlem0  35262  xoromon  35767  fineqvomonb  35843  noinfepfnregs  35856  subfacp1lem1  36030  fmlaomn0  36241  gonan0  36243  goaln0  36244  fmla0disjsuc  36249  ex-sategoelelomsuc  36277  ex-sategoelel12  36278  prv1n  36282  bcneg1  36593  opelco3  36631  wsuclem  36679  dfrdg4  36807  linedegen  37000  rankeq1o  37024  hfninf  37027  ordcmp  37327  curryset  37951  currysetlem3  37954  bj-projval  38001  bj-inftyexpitaudisj  38219  bj-inftyexpidisj  38224  irrdiff  38340  relowlpssretop  38380  finxpreclem2  38406  finxpreclem3  38409  finxpreclem5  38411  nlpineqsn  38424  poimirlem18  38649  poimirlem19  38650  poimirlem20  38651  mblfinlem1  38668  suceldisj  39843  elpadd0  40959  pssn0  43374  oexpreposd  43472  diophin  43876  fiphp3d  43919  expdioph  44123  wepwsolem  44142  kelac1  44158  onov0suclim  44369  tfsconcatb0  44439  ensucne0  44623  relintabex  44675  brnonrel  44682  relexp01min  44806  iooinlbub  46606  stoweidlem34  47137  fourierdlem60  47269  fourierdlem61  47270  afv20defat  48395  minusmodnep2tmod  48522  spr0nelg  48651  sprsymrelfvlem  48665  fmtnoinf  48714  fmtno4prmfac193  48751  fmtno4prm  48753  31prm  48775  lighneallem3  48785  lighneallem4  48788  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  dig2nn1st  49810  itcoval1  49868  line2ylem  49956  ipolub00  50200  fucofvalne  50540