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  4038  nel02  4288  sbcel12  4372  sbcel2  4379  sbcbr123  5163  sbcbr  5164  axnul  5262  intex  5309  intnex  5310  iin0  5328  notsep  5329  nfcvb  5342  eunex  5356  opelopabsb  5508  brabv  5545  epelg  5556  0nelelxp  5690  elimasni  6101  onxpdisj  6508  ndmfvrcl  6941  canth  7397  oprssdm  7626  ndmovrcl  7631  omelon2  7914  poxp2  8187  xpord2indlem  8191  poxp3  8194  undefnel2  8323  tfr2b  8432  tz7.44-3  8444  nlim2  8526  ord1eln01  8532  ord2eln012  8533  1ellim  8534  2ellim  8535  eceqoveq  8871  2dom  9086  omxpenlem  9125  domunsn  9174  disjen  9181  infensuc  9202  ordfin  9259  0sdom1dom  9265  1sdom2dom  9273  infn0  9322  elfi2  9433  en3lp  9642  preleqALT  9645  rankxpsuc  9926  updjudhcoinrg  10041  sdomsdomcardi  10079  cardmin2  10107  pm54.43lem  10108  pr2ne  10111  alephgeom  10188  alephval3  10216  cfsuc  10362  cflim2  10368  alephval2  10684  axunnd  10708  canthp1lem1  10764  pwxpndom2  10777  rankcf  10889  pinq  11039  adderpq  11068  mulerpq  11069  nqpr  11126  ltsopr  11144  ltapr  11157  renepnf  11384  renemnf  11385  lt0ne0d  11908  prodgt0  12191  nnne0ALT  12403  nn0nepnf  12714  xrltnr  13275  pnfnlt  13284  nltmnf  13285  xrltnsym  13293  nltpnft  13321  ngtmnft  13323  xsubge0  13418  xmullem2  13422  xlemul1a  13445  xrsupsslem  13464  xrinfmsslem  13465  xrub  13469  fzpreddisj  13734  fzm1  13768  uzinf  14135  hashnemnf  14515  hashclb  14529  hasheq0  14534  hashnn0n0nn  14562  prprrab  14645  tpf1ofv1  14669  tpf1ofv2  14670  lsw0  14737  cats1un  14898  geolim  16068  geolim2  16069  georeclim  16070  geoisumr  16076  m1exp1  16575  bitsfzolem  16633  bitsfzo  16634  bitsinv1lem  16640  sadcp1  16654  saddisjlem  16663  smu01lem  16684  3prm  16898  pcgcd1  17084  pc2dvds  17086  pcmpt  17099  prmreclem5  17127  vdwap0  17183  prmo1  17244  fvprif  17762  setcepi  18292  oduclatb  18710  chnccats1  18828  chnccat  18829  smndex1n0mnd  19140  cntzrcl  19571  pmtrfrn  19702  pmtrprfval  19731  pmtrprfvalrn  19732  psgnunilem5  19738  odhash3  19820  gsumzaddlem  20165  gsumzsplit  20171  dprdcntz2  20284  trivnsimpgd  20343  0ringnnzr  20806  xrsdsreclblem  21749  dsmmfi  22074  islindf4  22174  mplcoe1  22376  mplcoe5  22379  psrbagsn  22402  pmatcollpw3fi1lem1  23134  istps  23282  haust1  23700  hauspwdom  23850  kqcldsat  24082  csdfil  24243  tsmssplit  24501  dscopn  24922  htpycc  25331  pco1  25366  pcohtpylem  25370  pcopt  25373  pcopt2  25374  pcoass  25375  pcorevlem  25377  itg11  26042  bddmulibl  26189  lhop1  26364  deg1nn0clb  26438  plypf1  26561  plyn0mulidp  26632  vieta1lem2  26664  logdmn0  26998  logcnlem3  27002  fsumharmonic  27369  sqff1o  27539  perfectlem1  27586  bposlem5  27645  lgsval2lem  27664  addsqrexnreu  27799  addsqnreup  27800  ostth  27996  ltsval2  28043  ltsintdifex  28048  ltsres  28049  nolt02o  28082  nogt01o  28083  bday1  28230  lrold  28313  lrrecpo  28357  mulsval  28525  legso  29092  axlowdimlem13  29562  axlowdimlem16  29565  axlowdim1  29567  axlowdim  29569  upgrfi  29699  lfgrnloop  29733  umgredgnlp  29755  wlkp1lem3  30284  rusgrnumwwlkl1  30590  clwwlk  30604  clwwlkn0  30649  clwwlknon1sn  30721  trlsegvdeg  30858  konigsberg  30888  ex-res  31072  norm1exi  31882  dmadjrnb  32538  strlem1  32882  largei  32899  ifeqeqx  33210  ubico  33437  expgt0b  33478  0ringirng  34391  rtelextdg2lem  34428  2sqr3minply  34482  dya2iocuni  34985  eulerpartlemgh  35080  ballotlem4  35201  signswch  35260  signstfvneq0  35271  signlem0  35286  xoromon  35794  fineqvomonb  35887  noinfepfnregs  35900  subfacp1lem1  36111  fmlaomn0  36322  gonan0  36324  goaln0  36325  fmla0disjsuc  36330  ex-sategoelelomsuc  36358  ex-sategoelel12  36359  prv1n  36363  bcneg1  36679  opelco3  36717  wsuclem  36765  dfrdg4  36893  linedegen  37086  rankeq1o  37110  hfninf  37113  ordcmp  37413  curryset  38037  currysetlem3  38040  bj-projval  38087  bj-inftyexpitaudisj  38318  bj-inftyexpidisj  38323  irrdiff  38439  relowlpssretop  38479  finxpreclem2  38505  finxpreclem3  38508  finxpreclem5  38510  nlpineqsn  38523  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  mblfinlem1  38767  suceldisj  39942  elpadd0  41058  pssn0  43474  oexpreposd  43572  diophin  43976  fiphp3d  44019  expdioph  44223  wepwsolem  44242  kelac1  44258  onov0suclim  44468  tfsconcatb0  44538  ensucne0  44722  relintabex  44774  brnonrel  44781  relexp01min  44905  iooinlbub  46718  stoweidlem34  47249  fourierdlem60  47381  fourierdlem61  47382  afv20defat  48507  minusmodnep2tmod  48634  spr0nelg  48763  sprsymrelfvlem  48777  fmtnoinf  48826  fmtno4prmfac193  48863  fmtno4prm  48865  31prm  48887  lighneallem3  48897  lighneallem4  48900  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  dig2nn1st  49922  itcoval1  49980  line2ylem  50068  ipolub00  50312  fucofvalne  50652