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  4047  nel02  4279  sbcel12  4351  sbcel2  4358  sbcbr123  5139  sbcbr  5140  axnul  5240  intex  5285  intnex  5286  iin0  5304  notzfaus  5305  nfcvb  5318  eunex  5332  opelopabsb  5485  brabv  5521  epelg  5532  0nelelxp  5666  elimasni  6056  onxpdisj  6450  ndmfvrcl  6873  canth  7321  oprssdm  7548  ndmovrcl  7553  omelon2  7830  poxp2  8093  xpord2indlem  8097  poxp3  8100  undefnel2  8227  tfr2b  8335  tz7.44-3  8347  nlim2  8425  ord1eln01  8431  ord2eln012  8432  1ellim  8433  2ellim  8434  eceqoveq  8769  2dom  8977  omxpenlem  9016  domunsn  9065  disjen  9072  infensuc  9093  ordfin  9150  0sdom1dom  9156  1sdom2dom  9164  infn0  9212  elfi2  9327  en3lp  9535  preleqALT  9538  rankxpsuc  9806  updjudhcoinrg  9857  sdomsdomcardi  9895  cardmin2  9923  pm54.43lem  9924  pr2ne  9927  alephgeom  10004  alephval3  10032  cfsuc  10179  cflim2  10185  alephval2  10495  axunnd  10519  canthp1lem1  10575  pwxpndom2  10588  rankcf  10700  pinq  10850  adderpq  10879  mulerpq  10880  nqpr  10937  ltsopr  10955  ltapr  10968  renepnf  11193  renemnf  11194  lt0ne0d  11715  prodgt0  12002  nnne0ALT  12215  nn0nepnf  12518  xrltnr  13070  pnfnlt  13079  nltmnf  13080  xrltnsym  13088  nltpnft  13116  ngtmnft  13118  xsubge0  13213  xmullem2  13217  xlemul1a  13240  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  fzpreddisj  13527  fzm1  13561  uzinf  13927  hashnemnf  14306  hashclb  14320  hasheq0  14325  hashnn0n0nn  14353  prprrab  14435  tpf1ofv1  14459  tpf1ofv2  14460  lsw0  14527  cats1un  14683  geolim  15835  geolim2  15836  georeclim  15837  geoisumr  15843  m1exp1  16345  bitsfzolem  16403  bitsfzo  16404  bitsinv1lem  16410  sadcp1  16424  saddisjlem  16433  smu01lem  16454  3prm  16663  pcgcd1  16848  pc2dvds  16850  pcmpt  16863  prmreclem5  16891  vdwap0  16947  prmo1  17008  fvprif  17525  setcepi  18055  oduclatb  18473  chnccats1  18591  chnccat  18592  smndex1n0mnd  18883  cntzrcl  19302  pmtrfrn  19433  pmtrprfval  19462  pmtrprfvalrn  19463  psgnunilem5  19469  odhash3  19551  gsumzaddlem  19896  gsumzsplit  19902  dprdcntz2  20015  trivnsimpgd  20074  0ringnnzr  20502  xrsdsreclblem  21393  dsmmfi  21718  islindf4  21818  mplcoe1  22015  mplcoe5  22018  psrbagsn  22041  pmatcollpw3fi1lem1  22751  istps  22899  haust1  23317  hauspwdom  23466  kqcldsat  23698  csdfil  23859  tsmssplit  24117  dscopn  24538  htpycc  24947  pco1  24982  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  itg11  25658  bddmulibl  25806  lhop1  25981  deg1nn0clb  26055  plypf1  26177  vieta1lem2  26277  logdmn0  26604  logcnlem3  26608  fsumharmonic  26975  sqff1o  27145  perfectlem1  27192  bposlem5  27251  lgsval2lem  27270  addsqrexnreu  27405  addsqnreup  27406  ostth  27602  ltsval2  27620  ltsintdifex  27625  ltsres  27626  nolt02o  27659  nogt01o  27660  bday1  27806  lrold  27889  lrrecpo  27933  mulsval  28101  legso  28667  axlowdimlem13  29023  axlowdimlem16  29026  axlowdim1  29028  axlowdim  29030  upgrfi  29160  lfgrnloop  29194  umgredgnlp  29216  wlkp1lem3  29742  rusgrnumwwlkl1  30039  clwwlk  30053  clwwlkn0  30098  clwwlknon1sn  30170  trlsegvdeg  30297  konigsberg  30327  ex-res  30511  norm1exi  31321  dmadjrnb  31977  strlem1  32321  largei  32338  ifeqeqx  32612  ubico  32848  expgt0b  32890  0ringirng  33833  rtelextdg2lem  33870  2sqr3minply  33924  dya2iocuni  34427  eulerpartlemgh  34522  ballotlem4  34643  plymulx0  34691  signswch  34705  signstfvneq0  34716  signlem0  34731  xoromon  35232  fineqvomonb  35263  noinfepfnregs  35276  subfacp1lem1  35361  fmlaomn0  35572  gonan0  35574  goaln0  35575  fmla0disjsuc  35580  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  prv1n  35613  bcneg1  35918  opelco3  35957  wsuclem  36005  dfrdg4  36133  linedegen  36325  rankeq1o  36353  hfninf  36368  ordcmp  36629  curryset  37253  currysetlem3  37256  bj-projval  37303  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  irrdiff  37640  relowlpssretop  37680  finxpreclem2  37706  finxpreclem3  37709  finxpreclem5  37711  nlpineqsn  37724  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  mblfinlem1  37978  suceldisj  39139  elpadd0  40255  pssn0  42668  oexpreposd  42754  diophin  43204  fiphp3d  43247  expdioph  43451  wepwsolem  43470  kelac1  43491  onov0suclim  43702  tfsconcatb0  43772  ensucne0  43956  relintabex  44008  brnonrel  44016  relexp01min  44140  iooinlbub  45931  stoweidlem34  46462  fourierdlem60  46594  fourierdlem61  46595  afv20defat  47680  minusmodnep2tmod  47807  spr0nelg  47936  sprsymrelfvlem  47950  fmtnoinf  47999  fmtno4prmfac193  48036  fmtno4prm  48038  31prm  48060  lighneallem3  48070  lighneallem4  48073  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  dig2nn1st  49081  itcoval1  49139  line2ylem  49227  ipolub00  49468  fucofvalne  49800