Theorem mtbiri 681

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 670	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3499  n0i  3500  axnul  4214  intexr  4240  intnexr  4241  iin0r  4259  exmid01  4288  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  sucprcreg  4647  preleq  4653  reg3exmidlemwe  4677  dcextest  4679  nn0eln0  4718  0nelelxp  4754  canth  5969  tfrlemisucaccv  6491  nnsucuniel  6663  nndceq  6667  nndcel  6668  2dom  6980  snnen2oprc  7046  snexxph  7149  elfi2  7171  djune  7277  updjudhcoinrg  7280  omp1eomlem  7293  nnnninfeq  7327  ismkvnex  7354  mkvprop  7357  omniwomnimkv  7366  nninfwlpoimlemginf  7375  exmidfodomrlemrALT  7414  exmidaclem  7423  netap  7473  2omotaplemap  7476  elni2  7534  ltsopi  7540  ltsonq  7618  renepnf  8227  renemnf  8228  lt0ne0d  8693  sup3exmid  9137  nnne0  9171  nn0ge2m1nn  9462  nn0nepnf  9473  xrltnr  10014  pnfnlt  10022  nltmnf  10023  xrltnsym  10028  xrlttri3  10032  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xrpnfdc  10077  xrmnfdc  10078  xsubge0  10116  xposdif  10117  xleaddadd  10122  fzpreddisj  10306  fzm1  10335  exfzdc  10487  xnn0nnen  10700  lsw0  11162  cats1un  11303  xrbdtri  11838  m1exp1  12464  bitsfzolem  12517  bitsfzo  12518  bitsinv1lem  12524  3prm  12702  prmdc  12704  pcgcd1  12903  pc2dvds  12905  pcmpt  12918  exmidunben  13049  unct  13065  fvprif  13428  blssioo  15280  pilem3  15510  perfectlem1  15726  lgsval2lem  15742  umgredgnlp  16006  clwwlkn0  16262  clwwlknnn  16266  trlsegvdegfi  16321  eupth2lem3lem4fi  16327  bj-charfunbi  16427  bj-intexr  16524  bj-intnexr  16525  3dom  16608  2omap  16615  subctctexmid  16622  nninfsellemeq  16637  exmidsbthrlem  16647