Theorem mtbiri 329

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

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

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 209

This theorem is referenced by:  psstr  4081  nel02  4298  n0i  4299  sbcel12  4360  sbcel2  4367  sbcbr123  5120  sbcbr  5121  axnul  5209  intex  5240  intnex  5241  iin0  5261  notzfaus  5262  nfcvb  5277  eunex  5291  opelopabsb  5417  brabv  5453  epelg  5466  0nelelxp  5590  elimasni  5956  0ellim  6253  onxpdisj  6310  ndmfvrcl  6701  canth  7111  fvmptopab  7209  oprssdm  7329  ndmovrcl  7334  omelon2  7592  undefnel2  7943  tfr2b  8032  tz7.44-3  8044  eceqoveq  8402  2dom  8582  omxpenlem  8618  domunsn  8667  disjen  8674  infensuc  8695  snnen2o  8707  elfi2  8878  en3lp  9077  preleqALT  9080  rankxpsuc  9311  updjudhcoinrg  9362  sdomsdomcardi  9400  cardmin2  9427  pm54.43lem  9428  alephgeom  9508  alephval3  9536  cfsuc  9679  cflim2  9685  alephval2  9994  axunnd  10018  canthp1lem1  10074  pwxpndom2  10087  rankcf  10199  pinq  10349  adderpq  10378  mulerpq  10379  nqpr  10436  ltsopr  10454  ltapr  10467  renepnf  10689  renemnf  10690  lt0ne0d  11205  prodgt0  11487  nnne0ALT  11676  nn0nepnf  11976  xrltnr  12515  pnfnlt  12524  nltmnf  12525  xrltnsym  12531  nltpnft  12558  ngtmnft  12560  xsubge0  12655  xmullem2  12659  xlemul1a  12682  xrsupsslem  12701  xrinfmsslem  12702  xrub  12706  fzpreddisj  12957  fzm1  12988  uzinf  13334  hashnemnf  13705  hashclb  13720  hasheq0  13725  hashnn0n0nn  13753  prprrab  13832  lsw0  13917  cats1un  14083  geolim  15226  geolim2  15227  georeclim  15228  geoisumr  15234  m1exp1  15727  bitsfzolem  15783  bitsfzo  15784  bitsinv1lem  15790  sadcp1  15804  saddisjlem  15813  smu01lem  15834  3prm  16038  pcgcd1  16213  pc2dvds  16215  pcmpt  16228  prmreclem5  16256  vdwap0  16312  prmo1  16373  fvprif  16834  setcepi  17348  oduclatb  17754  smndex1n0mnd  18077  cntzrcl  18457  pmtrfrn  18586  pmtrprfval  18615  pmtrprfvalrn  18616  psgnunilem5  18622  odhash3  18701  gsumzaddlem  19041  gsumzsplit  19047  dprdcntz2  19160  trivnsimpgd  19219  0ringnnzr  20042  mplcoe1  20246  mplcoe5  20249  psrbagsn  20275  xrsdsreclblem  20591  dsmmfi  20882  islindf4  20982  pmatcollpw3fi1lem1  21394  istps  21542  haust1  21960  hauspwdom  22109  kqcldsat  22341  csdfil  22502  tsmssplit  22760  dscopn  23183  htpycc  23584  pco1  23619  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  itg11  24292  bddmulibl  24439  lhop1  24611  deg1nn0clb  24684  plypf1  24802  vieta1lem2  24900  logdmn0  25223  logcnlem3  25227  fsumharmonic  25589  sqff1o  25759  perfectlem1  25805  bposlem5  25864  lgsval2lem  25883  addsqrexnreu  26018  addsqnreup  26019  ostth  26215  legso  26385  axlowdimlem13  26740  axlowdimlem16  26743  axlowdim1  26745  axlowdim  26747  upgrfi  26876  lfgrnloop  26910  umgredgnlp  26932  wlkp1lem3  27457  rusgrnumwwlkl1  27747  clwwlk  27761  clwwlkn0  27806  clwwlknon1sn  27879  trlsegvdeg  28006  konigsberg  28036  ex-res  28220  norm1exi  29027  dmadjrnb  29683  strlem1  30027  largei  30044  ifeqeqx  30297  ubico  30498  dya2iocuni  31541  eulerpartlemgh  31636  ballotlem4  31756  plymulx0  31817  signswch  31831  signstfvneq0  31842  signlem0  31857  subfacp1lem1  32426  fmlaomn0  32637  gonan0  32639  goaln0  32640  fmla0disjsuc  32645  ex-sategoelelomsuc  32673  ex-sategoelel12  32674  prv1n  32678  bcneg1  32968  opelco3  33018  wsuclem  33112  sltval2  33163  sltintdifex  33168  sltres  33169  nolt02o  33199  dfrdg4  33412  linedegen  33604  rankeq1o  33632  hfninf  33647  ordcmp  33795  curryset  34260  currysetlem3  34263  bj-projval  34311  bj-inftyexpitaudisj  34490  bj-inftyexpidisj  34495  relowlpssretop  34648  finxpreclem2  34674  finxpreclem3  34677  finxpreclem5  34679  nlpineqsn  34692  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  mblfinlem1  34944  elpadd0  36960  pssn0  39162  oexpreposd  39228  diophin  39418  fiphp3d  39465  expdioph  39669  wepwsolem  39691  kelac1  39712  ensucne0  39944  relintabex  39990  brnonrel  39998  relexp01min  40107  iooinlbub  41825  stoweidlem34  42368  fourierdlem60  42500  fourierdlem61  42501  afv20defat  43480  spr0nelg  43687  sprsymrelfvlem  43701  fmtnoinf  43747  fmtno4prmfac193  43784  fmtno4prm  43786  31prm  43809  lighneallem3  43821  lighneallem4  43824  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  dig2nn1st  44714  line2ylem  44787