Theorem mtbiri 677

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 666	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3466  n0i  3467  axnul  4173  intexr  4198  intnexr  4199  iin0r  4217  exmid01  4246  ordtriexmidlem  4571  ordtriexmidlem2  4572  ordtri2or2exmidlem  4578  onsucelsucexmidlem  4581  sucprcreg  4601  preleq  4607  reg3exmidlemwe  4631  dcextest  4633  nn0eln0  4672  0nelelxp  4708  canth  5904  tfrlemisucaccv  6418  nnsucuniel  6588  nndceq  6592  nndcel  6593  2dom  6904  snnen2oprc  6964  snexxph  7059  elfi2  7081  djune  7187  updjudhcoinrg  7190  omp1eomlem  7203  nnnninfeq  7237  ismkvnex  7264  mkvprop  7267  omniwomnimkv  7276  nninfwlpoimlemginf  7285  exmidfodomrlemrALT  7318  exmidaclem  7327  netap  7373  2omotaplemap  7376  elni2  7434  ltsopi  7440  ltsonq  7518  renepnf  8127  renemnf  8128  lt0ne0d  8593  sup3exmid  9037  nnne0  9071  nn0ge2m1nn  9362  nn0nepnf  9373  xrltnr  9908  pnfnlt  9916  nltmnf  9917  xrltnsym  9922  xrlttri3  9926  nltpnft  9943  ngtmnft  9946  xrrebnd  9948  xrpnfdc  9971  xrmnfdc  9972  xsubge0  10010  xposdif  10011  xleaddadd  10016  fzpreddisj  10200  fzm1  10229  exfzdc  10376  xnn0nnen  10589  lsw0  11048  xrbdtri  11631  m1exp1  12256  bitsfzolem  12309  bitsfzo  12310  bitsinv1lem  12316  3prm  12494  prmdc  12496  pcgcd1  12695  pc2dvds  12697  pcmpt  12710  exmidunben  12841  unct  12857  fvprif  13219  blssioo  15069  pilem3  15299  perfectlem1  15515  lgsval2lem  15531  bj-charfunbi  15821  bj-intexr  15918  bj-intnexr  15919  2omap  16006  subctctexmid  16011  nninfsellemeq  16025  exmidsbthrlem  16035