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  4105  nel02  4333  n0i  4334  sbcel12  4409  sbcel2  4416  sbcbr123  5203  sbcbr  5204  axnul  5306  intex  5338  intnex  5339  iin0  5361  notzfaus  5362  nfcvb  5375  eunex  5389  opelopabsb  5531  brabv  5570  epelg  5582  0nelelxp  5712  elimasni  6091  0ellim  6428  onxpdisj  6491  ndmfvrcl  6928  canth  7362  fvmptopabOLD  7464  oprssdm  7588  ndmovrcl  7593  omelon2  7868  poxp2  8129  xpord2indlem  8133  poxp3  8136  undefnel2  8262  tfr2b  8396  tz7.44-3  8408  nlim2  8490  ord1eln01  8496  ord2eln012  8497  1ellim  8498  2ellim  8499  eceqoveq  8816  2dom  9030  omxpenlem  9073  domunsn  9127  disjen  9134  infensuc  9155  snnen2oOLD  9227  0sdom1dom  9238  1sdom2dom  9247  infn0  9307  elfi2  9409  en3lp  9609  preleqALT  9612  rankxpsuc  9877  updjudhcoinrg  9928  sdomsdomcardi  9966  cardmin2  9994  pm54.43lem  9995  pr2ne  9999  alephgeom  10077  alephval3  10105  cfsuc  10252  cflim2  10258  alephval2  10567  axunnd  10591  canthp1lem1  10647  pwxpndom2  10660  rankcf  10772  pinq  10922  adderpq  10951  mulerpq  10952  nqpr  11009  ltsopr  11027  ltapr  11040  renepnf  11262  renemnf  11263  lt0ne0d  11779  prodgt0  12061  nnne0ALT  12250  nn0nepnf  12552  xrltnr  13099  pnfnlt  13108  nltmnf  13109  xrltnsym  13116  nltpnft  13143  ngtmnft  13145  xsubge0  13240  xmullem2  13244  xlemul1a  13267  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  fzpreddisj  13550  fzm1  13581  uzinf  13930  hashnemnf  14304  hashclb  14318  hasheq0  14323  hashnn0n0nn  14351  prprrab  14434  lsw0  14515  cats1un  14671  geolim  15816  geolim2  15817  georeclim  15818  geoisumr  15824  m1exp1  16319  bitsfzolem  16375  bitsfzo  16376  bitsinv1lem  16382  sadcp1  16396  saddisjlem  16405  smu01lem  16426  3prm  16631  pcgcd1  16810  pc2dvds  16812  pcmpt  16825  prmreclem5  16853  vdwap0  16909  prmo1  16970  fvprif  17507  setcepi  18038  oduclatb  18460  smndex1n0mnd  18793  cntzrcl  19191  pmtrfrn  19326  pmtrprfval  19355  pmtrprfvalrn  19356  psgnunilem5  19362  odhash3  19444  gsumzaddlem  19789  gsumzsplit  19795  dprdcntz2  19908  trivnsimpgd  19967  0ringnnzr  20302  xrsdsreclblem  20991  dsmmfi  21293  islindf4  21393  mplcoe1  21592  mplcoe5  21595  psrbagsn  21624  pmatcollpw3fi1lem1  22288  istps  22436  haust1  22856  hauspwdom  23005  kqcldsat  23237  csdfil  23398  tsmssplit  23656  dscopn  24082  htpycc  24496  pco1  24531  pcohtpylem  24535  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  itg11  25208  bddmulibl  25356  lhop1  25531  deg1nn0clb  25608  plypf1  25726  vieta1lem2  25824  logdmn0  26148  logcnlem3  26152  fsumharmonic  26516  sqff1o  26686  perfectlem1  26732  bposlem5  26791  lgsval2lem  26810  addsqrexnreu  26945  addsqnreup  26946  ostth  27142  sltval2  27159  sltintdifex  27164  sltres  27165  nolt02o  27198  nogt01o  27199  bday1s  27333  lrold  27392  lrrecpo  27427  mulsval  27568  legso  27881  axlowdimlem13  28243  axlowdimlem16  28246  axlowdim1  28248  axlowdim  28250  upgrfi  28382  lfgrnloop  28416  umgredgnlp  28438  wlkp1lem3  28963  rusgrnumwwlkl1  29253  clwwlk  29267  clwwlkn0  29312  clwwlknon1sn  29384  trlsegvdeg  29511  konigsberg  29541  ex-res  29725  norm1exi  30534  dmadjrnb  31190  strlem1  31534  largei  31551  ifeqeqx  31805  ubico  32017  0ringirng  32784  dya2iocuni  33313  eulerpartlemgh  33408  ballotlem4  33528  plymulx0  33589  signswch  33603  signstfvneq0  33614  signlem0  33629  subfacp1lem1  34201  fmlaomn0  34412  gonan0  34414  goaln0  34415  fmla0disjsuc  34420  ex-sategoelelomsuc  34448  ex-sategoelel12  34449  prv1n  34453  bcneg1  34737  opelco3  34777  wsuclem  34828  dfrdg4  34954  linedegen  35146  rankeq1o  35174  hfninf  35189  ordcmp  35380  curryset  35875  currysetlem3  35878  bj-projval  35925  bj-inftyexpitaudisj  36134  bj-inftyexpidisj  36139  irrdiff  36255  relowlpssretop  36293  finxpreclem2  36319  finxpreclem3  36322  finxpreclem5  36324  nlpineqsn  36337  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  mblfinlem1  36573  elpadd0  38728  pssn0  41093  oexpreposd  41260  diophin  41558  fiphp3d  41605  expdioph  41810  wepwsolem  41832  kelac1  41853  onov0suclim  42072  tfsconcatb0  42142  ensucne0  42328  relintabex  42380  brnonrel  42388  relexp01min  42512  iooinlbub  44262  stoweidlem34  44798  fourierdlem60  44930  fourierdlem61  44931  tworepnotupword  45648  afv20defat  45988  spr0nelg  46192  sprsymrelfvlem  46206  fmtnoinf  46252  fmtno4prmfac193  46289  fmtno4prm  46291  31prm  46313  lighneallem3  46323  lighneallem4  46326  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  dig2nn1st  47339  itcoval1  47397  line2ylem  47485  ipolub00  47666