Theorem mtbiri 682

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  3512  n0i  3513  axnul  4234  intexr  4261  intnexr  4262  iin0r  4281  exmid01  4310  ordtriexmidlem  4640  ordtriexmidlem2  4641  ordtri2or2exmidlem  4647  onsucelsucexmidlem  4650  sucprcreg  4670  preleq  4676  reg3exmidlemwe  4700  dcextest  4702  nn0eln0  4741  0nelelxp  4777  canth  6000  tfrlemisucaccv  6555  nnsucuniel  6727  nndceq  6731  nndcel  6732  2dom  7045  snnen2oprc  7113  snexxph  7219  elfi2  7258  2omap  7268  djune  7368  updjudhcoinrg  7371  omp1eomlem  7384  nnnninfeq  7418  ismkvnex  7445  mkvprop  7448  omniwomnimkv  7457  nninfwlpoimlemginf  7466  exmidfodomrlemrALT  7505  exmidaclem  7514  netap  7564  2omotaplemap  7567  elni2  7625  ltsopi  7631  ltsonq  7709  renepnf  8317  renemnf  8318  lt0ne0d  8783  sup3exmid  9227  nnne0  9261  nn0ge2m1nn  9556  nn0nepnf  9567  xrltnr  10108  pnfnlt  10116  nltmnf  10117  xrltnsym  10122  xrlttri3  10126  nltpnft  10143  ngtmnft  10146  xrrebnd  10148  xrpnfdc  10171  xrmnfdc  10172  xsubge0  10210  xposdif  10211  xleaddadd  10216  fzpreddisj  10401  fzm1  10430  exfzdc  10582  xnn0nnen  10795  hashtpglem  11211  lsw0  11265  cats1un  11406  xrbdtri  11954  m1exp1  12580  bitsfzolem  12633  bitsfzo  12634  bitsinv1lem  12640  3prm  12818  prmdc  12820  pcgcd1  13019  pc2dvds  13021  pcmpt  13034  exmidunben  13166  unct  13182  fvprif  13545  blssioo  15405  pilem3  15635  perfectlem1  15854  lgsval2lem  15870  umgredgnlp  16134  clwwlkn0  16390  clwwlknnn  16394  trlsegvdegfi  16449  eupth2lem3lem4fi  16455  konigsberg  16475  bj-charfunbi  16568  bj-intexr  16665  bj-intnexr  16666  3dom  16749  subctctexmid  16761  nninfsellemeq  16779  exmidsbthrlem  16789