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  3496  n0i  3497  axnul  4209  intexr  4235  intnexr  4236  iin0r  4254  exmid01  4283  ordtriexmidlem  4612  ordtriexmidlem2  4613  ordtri2or2exmidlem  4619  onsucelsucexmidlem  4622  sucprcreg  4642  preleq  4648  reg3exmidlemwe  4672  dcextest  4674  nn0eln0  4713  0nelelxp  4749  canth  5961  tfrlemisucaccv  6482  nnsucuniel  6654  nndceq  6658  nndcel  6659  2dom  6971  snnen2oprc  7034  snexxph  7133  elfi2  7155  djune  7261  updjudhcoinrg  7264  omp1eomlem  7277  nnnninfeq  7311  ismkvnex  7338  mkvprop  7341  omniwomnimkv  7350  nninfwlpoimlemginf  7359  exmidfodomrlemrALT  7397  exmidaclem  7406  netap  7456  2omotaplemap  7459  elni2  7517  ltsopi  7523  ltsonq  7601  renepnf  8210  renemnf  8211  lt0ne0d  8676  sup3exmid  9120  nnne0  9154  nn0ge2m1nn  9445  nn0nepnf  9456  xrltnr  9992  pnfnlt  10000  nltmnf  10001  xrltnsym  10006  xrlttri3  10010  nltpnft  10027  ngtmnft  10030  xrrebnd  10032  xrpnfdc  10055  xrmnfdc  10056  xsubge0  10094  xposdif  10095  xleaddadd  10100  fzpreddisj  10284  fzm1  10313  exfzdc  10463  xnn0nnen  10676  lsw0  11137  cats1un  11274  xrbdtri  11808  m1exp1  12433  bitsfzolem  12486  bitsfzo  12487  bitsinv1lem  12493  3prm  12671  prmdc  12673  pcgcd1  12872  pc2dvds  12874  pcmpt  12887  exmidunben  13018  unct  13034  fvprif  13397  blssioo  15248  pilem3  15478  perfectlem1  15694  lgsval2lem  15710  umgredgnlp  15971  clwwlkn0  16177  clwwlknnn  16181  bj-charfunbi  16283  bj-intexr  16380  bj-intnexr  16381  3dom  16465  2omap  16472  subctctexmid  16479  nninfsellemeq  16494  exmidsbthrlem  16504