Theorem mtbiri 679

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3497  n0i  3498  axnul  4212  intexr  4238  intnexr  4239  iin0r  4257  exmid01  4286  ordtriexmidlem  4615  ordtriexmidlem2  4616  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  sucprcreg  4645  preleq  4651  reg3exmidlemwe  4675  dcextest  4677  nn0eln0  4716  0nelelxp  4752  canth  5964  tfrlemisucaccv  6486  nnsucuniel  6658  nndceq  6662  nndcel  6663  2dom  6975  snnen2oprc  7041  snexxph  7143  elfi2  7165  djune  7271  updjudhcoinrg  7274  omp1eomlem  7287  nnnninfeq  7321  ismkvnex  7348  mkvprop  7351  omniwomnimkv  7360  nninfwlpoimlemginf  7369  exmidfodomrlemrALT  7407  exmidaclem  7416  netap  7466  2omotaplemap  7469  elni2  7527  ltsopi  7533  ltsonq  7611  renepnf  8220  renemnf  8221  lt0ne0d  8686  sup3exmid  9130  nnne0  9164  nn0ge2m1nn  9455  nn0nepnf  9466  xrltnr  10007  pnfnlt  10015  nltmnf  10016  xrltnsym  10021  xrlttri3  10025  nltpnft  10042  ngtmnft  10045  xrrebnd  10047  xrpnfdc  10070  xrmnfdc  10071  xsubge0  10109  xposdif  10110  xleaddadd  10115  fzpreddisj  10299  fzm1  10328  exfzdc  10479  xnn0nnen  10692  lsw0  11154  cats1un  11295  xrbdtri  11830  m1exp1  12455  bitsfzolem  12508  bitsfzo  12509  bitsinv1lem  12515  3prm  12693  prmdc  12695  pcgcd1  12894  pc2dvds  12896  pcmpt  12909  exmidunben  13040  unct  13056  fvprif  13419  blssioo  15270  pilem3  15500  perfectlem1  15716  lgsval2lem  15732  umgredgnlp  15996  clwwlkn0  16217  clwwlknnn  16221  bj-charfunbi  16356  bj-intexr  16453  bj-intnexr  16454  3dom  16537  2omap  16544  subctctexmid  16551  nninfsellemeq  16566  exmidsbthrlem  16576