Theorem mtbiri 636

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-in1 580  ax-in2 581

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  n0i  3292  axnul  3970  intexr  3992  intnexr  3993  iin0r  4010  exmid01  4038  ordtriexmidlem  4349  ordtriexmidlem2  4350  ordtri2or2exmidlem  4355  onsucelsucexmidlem  4358  sucprcreg  4378  preleq  4384  reg3exmidlemwe  4407  dcextest  4409  nn0eln0  4446  0nelelxp  4480  tfrlemisucaccv  6104  nnsucuniel  6270  nndceq  6274  nndcel  6275  2dom  6576  snnen2oprc  6630  snexxph  6713  djune  6823  updjudhcoinrg  6826  exmidfodomrlemrALT  6890  elni2  6934  ltsopi  6940  ltsonq  7018  renepnf  7596  renemnf  7597  lt0ne0d  8052  nnne0  8511  nn0ge2m1nn  8794  nn0nepnf  8805  xrltnr  9311  pnfnlt  9318  nltmnf  9319  xrltnsym  9324  xrlttri3  9328  nltpnft  9340  ngtmnft  9341  xrrebnd  9342  fzpreddisj  9546  fzm1  9575  exfzdc  9712  m1exp1  11240  3prm  11449  bj-intexr  12072  bj-intnexr  12073  nninfalllemn  12170  nninfsellemeq  12178  exmidsbthrlem  12184