Theorem mtbiri 686

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 674	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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3526  n0i  3527  ifeqeqxdc  3687  axnul  4256  intexr  4284  intnexr  4285  iin0r  4304  exmid01  4333  ordtriexmidlem  4664  ordtriexmidlem2  4665  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  sucprcreg  4694  preleq  4700  reg3exmidlemwe  4724  dcextest  4726  nn0eln0  4765  0nelelxp  4801  canth  6030  tfrlemisucaccv  6590  nnsucuniel  6762  nndceq  6766  nndcel  6767  2dom  7087  snnen2oprc  7155  snexxph  7261  elfi2  7300  2omap  7312  djune  7412  updjudhcoinrg  7415  omp1eomlem  7428  nnnninfeq  7462  ismkvnex  7489  mkvprop  7492  omniwomnimkv  7501  nninfwlpoimlemginf  7510  exmidfodomrlemrALT  7549  exmidaclem  7558  netap  7614  2omotaplemap  7617  elni2  7675  ltsopi  7681  ltsonq  7759  renepnf  8367  renemnf  8368  lt0ne0d  8835  sup3exmid  9281  nnne0  9315  nn0ge2m1nn  9610  nn0nepnf  9621  xrltnr  10164  pnfnlt  10172  nltmnf  10173  xrltnsym  10178  xrlttri3  10182  nltpnft  10199  ngtmnft  10202  xrrebnd  10204  xrpnfdc  10227  xrmnfdc  10228  xsubge0  10266  xposdif  10267  xleaddadd  10272  fzpreddisj  10461  fzm1  10490  exfzdc  10642  xnn0nnen  10857  hashtpglem  11281  lsw0  11335  cats1un  11476  xrbdtri  12025  m1exp1  12651  bitsfzolem  12704  bitsfzo  12705  bitsinv1lem  12711  3prm  12889  prmdc  12891  pcgcd1  13090  pc2dvds  13092  pcmpt  13105  ballotfilem4  13224  exmidunben  13300  unct  13316  fvprif  13647  blssioo  15637  pilem3  15867  perfectlem1  16096  lgsval2lem  16112  umgredgnlp  16376  clwwlkn0  16632  clwwlknnn  16636  trlsegvdegfi  16691  eupth2lem3lem4fi  16697  konigsberg  16717  bj-charfunbi  16820  bj-intexr  16917  bj-intnexr  16918  3dom  17001  subctctexmid  17013  nninfsellemeq  17031  exmidsbthrlem  17041