Theorem mtbiri 676

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 665	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  3456  n0i  3457  axnul  4159  intexr  4184  intnexr  4185  iin0r  4203  exmid01  4232  ordtriexmidlem  4556  ordtriexmidlem2  4557  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  sucprcreg  4586  preleq  4592  reg3exmidlemwe  4616  dcextest  4618  nn0eln0  4657  0nelelxp  4693  canth  5878  tfrlemisucaccv  6392  nnsucuniel  6562  nndceq  6566  nndcel  6567  2dom  6873  snnen2oprc  6930  snexxph  7025  elfi2  7047  djune  7153  updjudhcoinrg  7156  omp1eomlem  7169  nnnninfeq  7203  ismkvnex  7230  mkvprop  7233  omniwomnimkv  7242  nninfwlpoimlemginf  7251  exmidfodomrlemrALT  7284  exmidaclem  7293  netap  7339  2omotaplemap  7342  elni2  7400  ltsopi  7406  ltsonq  7484  renepnf  8093  renemnf  8094  lt0ne0d  8559  sup3exmid  9003  nnne0  9037  nn0ge2m1nn  9328  nn0nepnf  9339  xrltnr  9873  pnfnlt  9881  nltmnf  9882  xrltnsym  9887  xrlttri3  9891  nltpnft  9908  ngtmnft  9911  xrrebnd  9913  xrpnfdc  9936  xrmnfdc  9937  xsubge0  9975  xposdif  9976  xleaddadd  9981  fzpreddisj  10165  fzm1  10194  exfzdc  10335  xnn0nnen  10548  xrbdtri  11460  m1exp1  12085  bitsfzolem  12138  bitsfzo  12139  bitsinv1lem  12145  3prm  12323  prmdc  12325  pcgcd1  12524  pc2dvds  12526  pcmpt  12539  exmidunben  12670  unct  12686  fvprif  13047  blssioo  14875  pilem3  15105  perfectlem1  15321  lgsval2lem  15337  bj-charfunbi  15543  bj-intexr  15640  bj-intnexr  15641  2omap  15728  subctctexmid  15733  nninfsellemeq  15747  exmidsbthrlem  15757