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  4234  intnexr  4235  iin0r  4253  exmid01  4282  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  sucprcreg  4641  preleq  4647  reg3exmidlemwe  4671  dcextest  4673  nn0eln0  4712  0nelelxp  4748  canth  5958  tfrlemisucaccv  6477  nnsucuniel  6649  nndceq  6653  nndcel  6654  2dom  6966  snnen2oprc  7029  snexxph  7125  elfi2  7147  djune  7253  updjudhcoinrg  7256  omp1eomlem  7269  nnnninfeq  7303  ismkvnex  7330  mkvprop  7333  omniwomnimkv  7342  nninfwlpoimlemginf  7351  exmidfodomrlemrALT  7389  exmidaclem  7398  netap  7448  2omotaplemap  7451  elni2  7509  ltsopi  7515  ltsonq  7593  renepnf  8202  renemnf  8203  lt0ne0d  8668  sup3exmid  9112  nnne0  9146  nn0ge2m1nn  9437  nn0nepnf  9448  xrltnr  9983  pnfnlt  9991  nltmnf  9992  xrltnsym  9997  xrlttri3  10001  nltpnft  10018  ngtmnft  10021  xrrebnd  10023  xrpnfdc  10046  xrmnfdc  10047  xsubge0  10085  xposdif  10086  xleaddadd  10091  fzpreddisj  10275  fzm1  10304  exfzdc  10454  xnn0nnen  10667  lsw0  11127  cats1un  11261  xrbdtri  11795  m1exp1  12420  bitsfzolem  12473  bitsfzo  12474  bitsinv1lem  12480  3prm  12658  prmdc  12660  pcgcd1  12859  pc2dvds  12861  pcmpt  12874  exmidunben  13005  unct  13021  fvprif  13384  blssioo  15235  pilem3  15465  perfectlem1  15681  lgsval2lem  15697  umgredgnlp  15958  bj-charfunbi  16198  bj-intexr  16295  bj-intnexr  16296  3dom  16381  2omap  16388  subctctexmid  16395  nninfsellemeq  16410  exmidsbthrlem  16420