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  4104  nel02  4332  n0i  4333  sbcel12  4408  sbcel2  4415  sbcbr123  5202  sbcbr  5203  axnul  5305  intex  5337  intnex  5338  iin0  5360  notzfaus  5361  nfcvb  5374  eunex  5388  opelopabsb  5530  brabv  5569  epelg  5581  0nelelxp  5711  elimasni  6088  0ellim  6425  onxpdisj  6488  ndmfvrcl  6925  canth  7359  fvmptopabOLD  7461  oprssdm  7585  ndmovrcl  7590  omelon2  7865  poxp2  8126  xpord2indlem  8130  poxp3  8133  undefnel2  8259  tfr2b  8393  tz7.44-3  8405  nlim2  8487  ord1eln01  8493  ord2eln012  8494  1ellim  8495  2ellim  8496  eceqoveq  8813  2dom  9027  omxpenlem  9070  domunsn  9124  disjen  9131  infensuc  9152  snnen2oOLD  9224  0sdom1dom  9235  1sdom2dom  9244  infn0  9304  elfi2  9406  en3lp  9606  preleqALT  9609  rankxpsuc  9874  updjudhcoinrg  9925  sdomsdomcardi  9963  cardmin2  9991  pm54.43lem  9992  pr2ne  9996  alephgeom  10074  alephval3  10102  cfsuc  10249  cflim2  10255  alephval2  10564  axunnd  10588  canthp1lem1  10644  pwxpndom2  10657  rankcf  10769  pinq  10919  adderpq  10948  mulerpq  10949  nqpr  11006  ltsopr  11024  ltapr  11037  renepnf  11259  renemnf  11260  lt0ne0d  11776  prodgt0  12058  nnne0ALT  12247  nn0nepnf  12549  xrltnr  13096  pnfnlt  13105  nltmnf  13106  xrltnsym  13113  nltpnft  13140  ngtmnft  13142  xsubge0  13237  xmullem2  13241  xlemul1a  13264  xrsupsslem  13283  xrinfmsslem  13284  xrub  13288  fzpreddisj  13547  fzm1  13578  uzinf  13927  hashnemnf  14301  hashclb  14315  hasheq0  14320  hashnn0n0nn  14348  prprrab  14431  lsw0  14512  cats1un  14668  geolim  15813  geolim2  15814  georeclim  15815  geoisumr  15821  m1exp1  16316  bitsfzolem  16372  bitsfzo  16373  bitsinv1lem  16379  sadcp1  16393  saddisjlem  16402  smu01lem  16423  3prm  16628  pcgcd1  16807  pc2dvds  16809  pcmpt  16822  prmreclem5  16850  vdwap0  16906  prmo1  16967  fvprif  17504  setcepi  18035  oduclatb  18457  smndex1n0mnd  18790  cntzrcl  19186  pmtrfrn  19321  pmtrprfval  19350  pmtrprfvalrn  19351  psgnunilem5  19357  odhash3  19439  gsumzaddlem  19784  gsumzsplit  19790  dprdcntz2  19903  trivnsimpgd  19962  0ringnnzr  20295  xrsdsreclblem  20984  dsmmfi  21285  islindf4  21385  mplcoe1  21584  mplcoe5  21587  psrbagsn  21616  pmatcollpw3fi1lem1  22280  istps  22428  haust1  22848  hauspwdom  22997  kqcldsat  23229  csdfil  23390  tsmssplit  23648  dscopn  24074  htpycc  24488  pco1  24523  pcohtpylem  24527  pcopt  24530  pcopt2  24531  pcoass  24532  pcorevlem  24534  itg11  25200  bddmulibl  25348  lhop1  25523  deg1nn0clb  25600  plypf1  25718  vieta1lem2  25816  logdmn0  26140  logcnlem3  26144  fsumharmonic  26506  sqff1o  26676  perfectlem1  26722  bposlem5  26781  lgsval2lem  26800  addsqrexnreu  26935  addsqnreup  26936  ostth  27132  sltval2  27149  sltintdifex  27154  sltres  27155  nolt02o  27188  nogt01o  27189  bday1s  27322  lrold  27381  lrrecpo  27415  mulsval  27555  legso  27840  axlowdimlem13  28202  axlowdimlem16  28205  axlowdim1  28207  axlowdim  28209  upgrfi  28341  lfgrnloop  28375  umgredgnlp  28397  wlkp1lem3  28922  rusgrnumwwlkl1  29212  clwwlk  29226  clwwlkn0  29271  clwwlknon1sn  29343  trlsegvdeg  29470  konigsberg  29500  ex-res  29684  norm1exi  30491  dmadjrnb  31147  strlem1  31491  largei  31508  ifeqeqx  31762  ubico  31974  0ringirng  32742  dya2iocuni  33271  eulerpartlemgh  33366  ballotlem4  33486  plymulx0  33547  signswch  33561  signstfvneq0  33572  signlem0  33587  subfacp1lem1  34159  fmlaomn0  34370  gonan0  34372  goaln0  34373  fmla0disjsuc  34378  ex-sategoelelomsuc  34406  ex-sategoelel12  34407  prv1n  34411  bcneg1  34695  opelco3  34735  wsuclem  34786  dfrdg4  34912  linedegen  35104  rankeq1o  35132  hfninf  35147  ordcmp  35321  curryset  35816  currysetlem3  35819  bj-projval  35866  bj-inftyexpitaudisj  36075  bj-inftyexpidisj  36080  irrdiff  36196  relowlpssretop  36234  finxpreclem2  36260  finxpreclem3  36263  finxpreclem5  36265  nlpineqsn  36278  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  mblfinlem1  36514  elpadd0  38669  pssn0  41042  oexpreposd  41208  diophin  41496  fiphp3d  41543  expdioph  41748  wepwsolem  41770  kelac1  41791  onov0suclim  42010  tfsconcatb0  42080  ensucne0  42266  relintabex  42318  brnonrel  42326  relexp01min  42450  iooinlbub  44201  stoweidlem34  44737  fourierdlem60  44869  fourierdlem61  44870  tworepnotupword  45587  afv20defat  45927  spr0nelg  46131  sprsymrelfvlem  46145  fmtnoinf  46191  fmtno4prmfac193  46228  fmtno4prm  46230  31prm  46252  lighneallem3  46262  lighneallem4  46265  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  dig2nn1st  47245  itcoval1  47303  line2ylem  47391  ipolub00  47572