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 ⊢ (𝜑 → ¬ 𝜓)

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

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 210

This theorem is referenced by:  psstr  4064  nel02  4294  sbcel12  4368  sbcel2  4375  sbcbr123  5159  sbcbr  5160  axnul  5260  intex  5305  intnex  5306  iin0  5324  notzfaus  5325  nfcvb  5338  eunex  5352  opelopabsb  5505  brabv  5542  epelg  5553  0nelelxp  5687  elimasni  6084  onxpdisj  6477  ndmfvrcl  6904  canth  7354  oprssdm  7581  ndmovrcl  7586  omelon2  7863  poxp2  8127  xpord2indlem  8131  poxp3  8134  undefnel2  8262  tfr2b  8371  tz7.44-3  8383  nlim2  8463  ord1eln01  8469  ord2eln012  8470  1ellim  8471  2ellim  8472  eceqoveq  8808  2dom  9015  omxpenlem  9054  domunsn  9103  disjen  9110  infensuc  9131  ordfin  9188  0sdom1dom  9194  1sdom2dom  9202  infn0  9250  elfi2  9362  en3lp  9571  preleqALT  9574  rankxpsuc  9842  updjudhcoinrg  9907  sdomsdomcardi  9945  cardmin2  9973  pm54.43lem  9974  pr2ne  9977  alephgeom  10054  alephval3  10082  cfsuc  10229  cflim2  10235  alephval2  10545  axunnd  10569  canthp1lem1  10625  pwxpndom2  10638  rankcf  10750  pinq  10900  adderpq  10929  mulerpq  10930  nqpr  10987  ltsopr  11005  ltapr  11018  renepnf  11245  renemnf  11246  lt0ne0d  11767  prodgt0  12053  nnne0ALT  12265  nn0nepnf  12576  xrltnr  13135  pnfnlt  13144  nltmnf  13145  xrltnsym  13153  nltpnft  13181  ngtmnft  13183  xsubge0  13278  xmullem2  13282  xlemul1a  13305  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  fzpreddisj  13592  fzm1  13626  uzinf  13992  hashnemnf  14371  hashclb  14385  hasheq0  14390  hashnn0n0nn  14418  prprrab  14500  tpf1ofv1  14524  tpf1ofv2  14525  lsw0  14592  cats1un  14748  geolim  15914  geolim2  15915  georeclim  15916  geoisumr  15922  m1exp1  16424  bitsfzolem  16482  bitsfzo  16483  bitsinv1lem  16489  sadcp1  16503  saddisjlem  16512  smu01lem  16533  3prm  16742  pcgcd1  16927  pc2dvds  16929  pcmpt  16942  prmreclem5  16970  vdwap0  17026  prmo1  17087  fvprif  17605  setcepi  18135  oduclatb  18553  chnccats1  18671  chnccat  18672  smndex1n0mnd  18964  cntzrcl  19388  pmtrfrn  19519  pmtrprfval  19548  pmtrprfvalrn  19549  psgnunilem5  19555  odhash3  19637  gsumzaddlem  19982  gsumzsplit  19988  dprdcntz2  20101  trivnsimpgd  20160  0ringnnzr  20600  xrsdsreclblem  21523  dsmmfi  21848  islindf4  21948  mplcoe1  22148  mplcoe5  22151  psrbagsn  22174  pmatcollpw3fi1lem1  22904  istps  23052  haust1  23470  hauspwdom  23619  kqcldsat  23851  csdfil  24012  tsmssplit  24270  dscopn  24691  htpycc  25100  pco1  25135  pcohtpylem  25139  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  itg11  25811  bddmulibl  25959  lhop1  26134  deg1nn0clb  26208  plypf1  26330  plyn0mulidp  26403  vieta1lem2  26433  logdmn0  26763  logcnlem3  26767  fsumharmonic  27134  sqff1o  27304  perfectlem1  27351  bposlem5  27410  lgsval2lem  27429  addsqrexnreu  27564  addsqnreup  27565  ostth  27761  ltsval2  27778  ltsintdifex  27783  ltsres  27784  nolt02o  27817  nogt01o  27818  bday1  27965  lrold  28048  lrrecpo  28092  mulsval  28260  legso  28826  axlowdimlem13  29213  axlowdimlem16  29216  axlowdim1  29218  axlowdim  29220  upgrfi  29350  lfgrnloop  29384  umgredgnlp  29406  wlkp1lem3  29932  rusgrnumwwlkl1  30229  clwwlk  30243  clwwlkn0  30288  clwwlknon1sn  30360  trlsegvdeg  30487  konigsberg  30517  ex-res  30701  norm1exi  31511  dmadjrnb  32167  strlem1  32511  largei  32528  ifeqeqx  32798  ubico  33032  expgt0b  33074  0ringirng  33996  rtelextdg2lem  34033  2sqr3minply  34087  dya2iocuni  34590  eulerpartlemgh  34685  ballotlem4  34806  signswch  34865  signstfvneq0  34876  signlem0  34891  xoromon  35394  fineqvomonb  35427  noinfepfnregs  35440  subfacp1lem1  35542  fmlaomn0  35753  gonan0  35755  goaln0  35756  fmla0disjsuc  35761  ex-sategoelelomsuc  35789  ex-sategoelel12  35790  prv1n  35794  bcneg1  36099  opelco3  36138  wsuclem  36186  dfrdg4  36314  linedegen  36506  rankeq1o  36534  hfninf  36549  ordcmp  36820  curryset  37443  currysetlem3  37446  bj-projval  37493  bj-inftyexpitaudisj  37709  bj-inftyexpidisj  37714  irrdiff  37830  relowlpssretop  37870  finxpreclem2  37896  finxpreclem3  37899  finxpreclem5  37901  nlpineqsn  37914  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  mblfinlem1  38168  suceldisj  39329  elpadd0  40445  pssn0  42858  oexpreposd  42943  diophin  43365  fiphp3d  43408  expdioph  43612  wepwsolem  43631  kelac1  43652  onov0suclim  43863  tfsconcatb0  43933  ensucne0  44117  relintabex  44169  brnonrel  44177  relexp01min  44301  iooinlbub  46075  stoweidlem34  46606  fourierdlem60  46738  fourierdlem61  46739  afv20defat  47824  minusmodnep2tmod  47951  spr0nelg  48080  sprsymrelfvlem  48094  fmtnoinf  48143  fmtno4prmfac193  48180  fmtno4prm  48182  31prm  48204  lighneallem3  48214  lighneallem4  48217  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  dig2nn1st  49236  itcoval1  49294  line2ylem  49382  ipolub00  49622  fucofvalne  49954