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  27332  lrold  27391  lrrecpo  27425  mulsval  27565  legso  27850  axlowdimlem13  28212  axlowdimlem16  28215  axlowdim1  28217  axlowdim  28219  upgrfi  28351  lfgrnloop  28385  umgredgnlp  28407  wlkp1lem3  28932  rusgrnumwwlkl1  29222  clwwlk  29236  clwwlkn0  29281  clwwlknon1sn  29353  trlsegvdeg  29480  konigsberg  29510  ex-res  29694  norm1exi  30503  dmadjrnb  31159  strlem1  31503  largei  31520  ifeqeqx  31774  ubico  31986  0ringirng  32753  dya2iocuni  33282  eulerpartlemgh  33377  ballotlem4  33497  plymulx0  33558  signswch  33572  signstfvneq0  33583  signlem0  33598  subfacp1lem1  34170  fmlaomn0  34381  gonan0  34383  goaln0  34384  fmla0disjsuc  34389  ex-sategoelelomsuc  34417  ex-sategoelel12  34418  prv1n  34422  bcneg1  34706  opelco3  34746  wsuclem  34797  dfrdg4  34923  linedegen  35115  rankeq1o  35143  hfninf  35158  ordcmp  35332  curryset  35827  currysetlem3  35830  bj-projval  35877  bj-inftyexpitaudisj  36086  bj-inftyexpidisj  36091  irrdiff  36207  relowlpssretop  36245  finxpreclem2  36271  finxpreclem3  36274  finxpreclem5  36276  nlpineqsn  36289  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  mblfinlem1  36525  elpadd0  38680  pssn0  41045  oexpreposd  41212  diophin  41510  fiphp3d  41557  expdioph  41762  wepwsolem  41784  kelac1  41805  onov0suclim  42024  tfsconcatb0  42094  ensucne0  42280  relintabex  42332  brnonrel  42340  relexp01min  42464  iooinlbub  44214  stoweidlem34  44750  fourierdlem60  44882  fourierdlem61  44883  tworepnotupword  45600  afv20defat  45940  spr0nelg  46144  sprsymrelfvlem  46158  fmtnoinf  46204  fmtno4prmfac193  46241  fmtno4prm  46243  31prm  46265  lighneallem3  46275  lighneallem4  46278  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  dig2nn1st  47291  itcoval1  47349  line2ylem  47437  ipolub00  47618