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

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

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 206

This theorem is referenced by:  psstr  4101  nel02  4329  n0i  4330  sbcel12  4405  sbcel2  4412  sbcbr123  5197  sbcbr  5198  axnul  5300  intex  5334  intnex  5335  iin0  5357  notzfaus  5358  nfcvb  5371  eunex  5385  opelopabsb  5527  brabv  5566  epelg  5578  0nelelxp  5708  elimasni  6090  0ellim  6427  onxpdisj  6490  ndmfvrcl  6928  canth  7368  fvmptopabOLD  7470  oprssdm  7597  ndmovrcl  7602  omelon2  7878  poxp2  8143  xpord2indlem  8147  poxp3  8150  undefnel2  8277  tfr2b  8411  tz7.44-3  8423  nlim2  8505  ord1eln01  8511  ord2eln012  8512  1ellim  8513  2ellim  8514  eceqoveq  8835  2dom  9049  omxpenlem  9092  domunsn  9146  disjen  9153  infensuc  9174  snnen2oOLD  9246  0sdom1dom  9257  1sdom2dom  9266  infn0  9326  elfi2  9432  en3lp  9632  preleqALT  9635  rankxpsuc  9900  updjudhcoinrg  9951  sdomsdomcardi  9989  cardmin2  10017  pm54.43lem  10018  pr2ne  10022  alephgeom  10100  alephval3  10128  cfsuc  10275  cflim2  10281  alephval2  10590  axunnd  10614  canthp1lem1  10670  pwxpndom2  10683  rankcf  10795  pinq  10945  adderpq  10974  mulerpq  10975  nqpr  11032  ltsopr  11050  ltapr  11063  renepnf  11287  renemnf  11288  lt0ne0d  11804  prodgt0  12086  nnne0ALT  12275  nn0nepnf  12577  xrltnr  13126  pnfnlt  13135  nltmnf  13136  xrltnsym  13143  nltpnft  13170  ngtmnft  13172  xsubge0  13267  xmullem2  13271  xlemul1a  13294  xrsupsslem  13313  xrinfmsslem  13314  xrub  13318  fzpreddisj  13577  fzm1  13608  uzinf  13957  hashnemnf  14330  hashclb  14344  hasheq0  14349  hashnn0n0nn  14377  prprrab  14461  lsw0  14542  cats1un  14698  geolim  15843  geolim2  15844  georeclim  15845  geoisumr  15851  m1exp1  16347  bitsfzolem  16403  bitsfzo  16404  bitsinv1lem  16410  sadcp1  16424  saddisjlem  16433  smu01lem  16454  3prm  16659  pcgcd1  16840  pc2dvds  16842  pcmpt  16855  prmreclem5  16883  vdwap0  16939  prmo1  17000  fvprif  17537  setcepi  18071  oduclatb  18493  smndex1n0mnd  18858  cntzrcl  19272  pmtrfrn  19407  pmtrprfval  19436  pmtrprfvalrn  19437  psgnunilem5  19443  odhash3  19525  gsumzaddlem  19870  gsumzsplit  19876  dprdcntz2  19989  trivnsimpgd  20048  0ringnnzr  20456  xrsdsreclblem  21339  dsmmfi  21666  islindf4  21766  mplcoe1  21969  mplcoe5  21972  psrbagsn  22001  pmatcollpw3fi1lem1  22682  istps  22830  haust1  23250  hauspwdom  23399  kqcldsat  23631  csdfil  23792  tsmssplit  24050  dscopn  24476  htpycc  24900  pco1  24936  pcohtpylem  24940  pcopt  24943  pcopt2  24944  pcoass  24945  pcorevlem  24947  itg11  25614  bddmulibl  25762  lhop1  25941  deg1nn0clb  26020  plypf1  26140  vieta1lem2  26240  logdmn0  26568  logcnlem3  26572  fsumharmonic  26938  sqff1o  27108  perfectlem1  27156  bposlem5  27215  lgsval2lem  27234  addsqrexnreu  27369  addsqnreup  27370  ostth  27566  sltval2  27583  sltintdifex  27588  sltres  27589  nolt02o  27622  nogt01o  27623  bday1s  27758  lrold  27817  lrrecpo  27852  mulsval  28003  legso  28397  axlowdimlem13  28759  axlowdimlem16  28762  axlowdim1  28764  axlowdim  28766  upgrfi  28898  lfgrnloop  28932  umgredgnlp  28954  wlkp1lem3  29483  rusgrnumwwlkl1  29773  clwwlk  29787  clwwlkn0  29832  clwwlknon1sn  29904  trlsegvdeg  30031  konigsberg  30061  ex-res  30245  norm1exi  31054  dmadjrnb  31710  strlem1  32054  largei  32071  ifeqeqx  32327  ubico  32538  0ringirng  33358  dya2iocuni  33898  eulerpartlemgh  33993  ballotlem4  34113  plymulx0  34174  signswch  34188  signstfvneq0  34199  signlem0  34214  subfacp1lem1  34784  fmlaomn0  34995  gonan0  34997  goaln0  34998  fmla0disjsuc  35003  ex-sategoelelomsuc  35031  ex-sategoelel12  35032  prv1n  35036  bcneg1  35325  opelco3  35365  wsuclem  35416  dfrdg4  35542  linedegen  35734  rankeq1o  35762  hfninf  35777  ordcmp  35926  curryset  36420  currysetlem3  36423  bj-projval  36470  bj-inftyexpitaudisj  36679  bj-inftyexpidisj  36684  irrdiff  36800  relowlpssretop  36838  finxpreclem2  36864  finxpreclem3  36867  finxpreclem5  36869  nlpineqsn  36882  poimirlem18  37106  poimirlem19  37107  poimirlem20  37108  mblfinlem1  37125  elpadd0  39277  pssn0  41706  oexpreposd  41872  diophin  42183  fiphp3d  42230  expdioph  42435  wepwsolem  42457  kelac1  42478  onov0suclim  42694  tfsconcatb0  42764  ensucne0  42950  relintabex  43002  brnonrel  43010  relexp01min  43134  iooinlbub  44877  stoweidlem34  45413  fourierdlem60  45545  fourierdlem61  45546  tworepnotupword  46263  afv20defat  46603  spr0nelg  46807  sprsymrelfvlem  46821  fmtnoinf  46867  fmtno4prmfac193  46904  fmtno4prm  46906  31prm  46928  lighneallem3  46938  lighneallem4  46941  nnsum4primeseven  47131  nnsum4primesevenALTV  47132  dig2nn1st  47669  itcoval1  47727  line2ylem  47815  ipolub00  47995

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »