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  4073  nel02  4305  n0i  4306  sbcel12  4377  sbcel2  4384  sbcbr123  5164  sbcbr  5165  axnul  5263  intex  5302  intnex  5303  iin0  5320  notzfaus  5321  nfcvb  5334  eunex  5348  opelopabsb  5493  brabv  5531  epelg  5542  0nelelxp  5676  elimasni  6065  onxpdisj  6463  ndmfvrcl  6897  canth  7344  fvmptopabOLD  7447  oprssdm  7573  ndmovrcl  7578  omelon2  7858  poxp2  8125  xpord2indlem  8129  poxp3  8132  undefnel2  8259  tfr2b  8367  tz7.44-3  8379  nlim2  8457  ord1eln01  8463  ord2eln012  8464  1ellim  8465  2ellim  8466  eceqoveq  8798  2dom  9004  omxpenlem  9047  domunsn  9097  disjen  9104  infensuc  9125  0sdom1dom  9192  1sdom2dom  9201  infn0  9258  elfi2  9372  en3lp  9574  preleqALT  9577  rankxpsuc  9842  updjudhcoinrg  9893  sdomsdomcardi  9931  cardmin2  9959  pm54.43lem  9960  pr2ne  9964  alephgeom  10042  alephval3  10070  cfsuc  10217  cflim2  10223  alephval2  10532  axunnd  10556  canthp1lem1  10612  pwxpndom2  10625  rankcf  10737  pinq  10887  adderpq  10916  mulerpq  10917  nqpr  10974  ltsopr  10992  ltapr  11005  renepnf  11229  renemnf  11230  lt0ne0d  11750  prodgt0  12036  nnne0ALT  12231  nn0nepnf  12530  xrltnr  13086  pnfnlt  13095  nltmnf  13096  xrltnsym  13104  nltpnft  13131  ngtmnft  13133  xsubge0  13228  xmullem2  13232  xlemul1a  13255  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  fzpreddisj  13541  fzm1  13575  uzinf  13937  hashnemnf  14316  hashclb  14330  hasheq0  14335  hashnn0n0nn  14363  prprrab  14445  tpf1ofv1  14469  tpf1ofv2  14470  lsw0  14537  cats1un  14693  geolim  15843  geolim2  15844  georeclim  15845  geoisumr  15851  m1exp1  16353  bitsfzolem  16411  bitsfzo  16412  bitsinv1lem  16418  sadcp1  16432  saddisjlem  16441  smu01lem  16462  3prm  16671  pcgcd1  16855  pc2dvds  16857  pcmpt  16870  prmreclem5  16898  vdwap0  16954  prmo1  17015  fvprif  17531  setcepi  18057  oduclatb  18473  smndex1n0mnd  18846  cntzrcl  19266  pmtrfrn  19395  pmtrprfval  19424  pmtrprfvalrn  19425  psgnunilem5  19431  odhash3  19513  gsumzaddlem  19858  gsumzsplit  19864  dprdcntz2  19977  trivnsimpgd  20036  0ringnnzr  20441  xrsdsreclblem  21336  dsmmfi  21654  islindf4  21754  mplcoe1  21951  mplcoe5  21954  psrbagsn  21977  pmatcollpw3fi1lem1  22680  istps  22828  haust1  23246  hauspwdom  23395  kqcldsat  23627  csdfil  23788  tsmssplit  24046  dscopn  24468  htpycc  24886  pco1  24922  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  itg11  25599  bddmulibl  25747  lhop1  25926  deg1nn0clb  26002  plypf1  26124  vieta1lem2  26226  logdmn0  26556  logcnlem3  26560  fsumharmonic  26929  sqff1o  27099  perfectlem1  27147  bposlem5  27206  lgsval2lem  27225  addsqrexnreu  27360  addsqnreup  27361  ostth  27557  sltval2  27575  sltintdifex  27580  sltres  27581  nolt02o  27614  nogt01o  27615  bday1s  27750  lrold  27815  lrrecpo  27855  mulsval  28019  legso  28533  axlowdimlem13  28888  axlowdimlem16  28891  axlowdim1  28893  axlowdim  28895  upgrfi  29025  lfgrnloop  29059  umgredgnlp  29081  wlkp1lem3  29610  rusgrnumwwlkl1  29905  clwwlk  29919  clwwlkn0  29964  clwwlknon1sn  30036  trlsegvdeg  30163  konigsberg  30193  ex-res  30377  norm1exi  31186  dmadjrnb  31842  strlem1  32186  largei  32203  ifeqeqx  32478  ubico  32705  expgt0b  32748  chnccats1  32948  0ringirng  33691  rtelextdg2lem  33723  2sqr3minply  33777  dya2iocuni  34281  eulerpartlemgh  34376  ballotlem4  34497  plymulx0  34545  signswch  34559  signstfvneq0  34570  signlem0  34585  subfacp1lem1  35173  fmlaomn0  35384  gonan0  35386  goaln0  35387  fmla0disjsuc  35392  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  prv1n  35425  bcneg1  35730  opelco3  35769  wsuclem  35820  dfrdg4  35946  linedegen  36138  rankeq1o  36166  hfninf  36181  ordcmp  36442  curryset  36941  currysetlem3  36944  bj-projval  36991  bj-inftyexpitaudisj  37200  bj-inftyexpidisj  37205  irrdiff  37321  relowlpssretop  37359  finxpreclem2  37385  finxpreclem3  37388  finxpreclem5  37390  nlpineqsn  37403  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  mblfinlem1  37658  elpadd0  39810  pssn0  42222  oexpreposd  42317  diophin  42767  fiphp3d  42814  expdioph  43019  wepwsolem  43038  kelac1  43059  onov0suclim  43270  tfsconcatb0  43340  ensucne0  43525  relintabex  43577  brnonrel  43585  relexp01min  43709  iooinlbub  45506  stoweidlem34  46039  fourierdlem60  46171  fourierdlem61  46172  tworepnotupword  46891  afv20defat  47237  minusmodnep2tmod  47358  spr0nelg  47481  sprsymrelfvlem  47495  fmtnoinf  47541  fmtno4prmfac193  47578  fmtno4prm  47580  31prm  47602  lighneallem3  47612  lighneallem4  47615  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  dig2nn1st  48598  itcoval1  48656  line2ylem  48744  ipolub00  48985  fucofvalne  49318