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  3476  n0i  3477  axnul  4188  intexr  4213  intnexr  4214  iin0r  4232  exmid01  4261  ordtriexmidlem  4588  ordtriexmidlem2  4589  ordtri2or2exmidlem  4595  onsucelsucexmidlem  4598  sucprcreg  4618  preleq  4624  reg3exmidlemwe  4648  dcextest  4650  nn0eln0  4689  0nelelxp  4725  canth  5925  tfrlemisucaccv  6441  nnsucuniel  6611  nndceq  6615  nndcel  6616  2dom  6928  snnen2oprc  6989  snexxph  7085  elfi2  7107  djune  7213  updjudhcoinrg  7216  omp1eomlem  7229  nnnninfeq  7263  ismkvnex  7290  mkvprop  7293  omniwomnimkv  7302  nninfwlpoimlemginf  7311  exmidfodomrlemrALT  7349  exmidaclem  7358  netap  7408  2omotaplemap  7411  elni2  7469  ltsopi  7475  ltsonq  7553  renepnf  8162  renemnf  8163  lt0ne0d  8628  sup3exmid  9072  nnne0  9106  nn0ge2m1nn  9397  nn0nepnf  9408  xrltnr  9943  pnfnlt  9951  nltmnf  9952  xrltnsym  9957  xrlttri3  9961  nltpnft  9978  ngtmnft  9981  xrrebnd  9983  xrpnfdc  10006  xrmnfdc  10007  xsubge0  10045  xposdif  10046  xleaddadd  10051  fzpreddisj  10235  fzm1  10264  exfzdc  10413  xnn0nnen  10626  lsw0  11085  cats1un  11219  xrbdtri  11753  m1exp1  12378  bitsfzolem  12431  bitsfzo  12432  bitsinv1lem  12438  3prm  12616  prmdc  12618  pcgcd1  12817  pc2dvds  12819  pcmpt  12832  exmidunben  12963  unct  12979  fvprif  13342  blssioo  15192  pilem3  15422  perfectlem1  15638  lgsval2lem  15654  umgredgnlp  15915  bj-charfunbi  16084  bj-intexr  16181  bj-intnexr  16182  2omap  16270  subctctexmid  16277  nninfsellemeq  16291  exmidsbthrlem  16301