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  3498  n0i  3499  axnul  4215  intexr  4241  intnexr  4242  iin0r  4261  exmid01  4290  ordtriexmidlem  4619  ordtriexmidlem2  4620  ordtri2or2exmidlem  4626  onsucelsucexmidlem  4629  sucprcreg  4649  preleq  4655  reg3exmidlemwe  4679  dcextest  4681  nn0eln0  4720  0nelelxp  4756  canth  5974  tfrlemisucaccv  6496  nnsucuniel  6668  nndceq  6672  nndcel  6673  2dom  6985  snnen2oprc  7051  snexxph  7154  elfi2  7176  djune  7282  updjudhcoinrg  7285  omp1eomlem  7298  nnnninfeq  7332  ismkvnex  7359  mkvprop  7362  omniwomnimkv  7371  nninfwlpoimlemginf  7380  exmidfodomrlemrALT  7419  exmidaclem  7428  netap  7478  2omotaplemap  7481  elni2  7539  ltsopi  7545  ltsonq  7623  renepnf  8232  renemnf  8233  lt0ne0d  8698  sup3exmid  9142  nnne0  9176  nn0ge2m1nn  9467  nn0nepnf  9478  xrltnr  10019  pnfnlt  10027  nltmnf  10028  xrltnsym  10033  xrlttri3  10037  nltpnft  10054  ngtmnft  10057  xrrebnd  10059  xrpnfdc  10082  xrmnfdc  10083  xsubge0  10121  xposdif  10122  xleaddadd  10127  fzpreddisj  10311  fzm1  10340  exfzdc  10492  xnn0nnen  10705  hashtpglem  11116  lsw0  11170  cats1un  11311  xrbdtri  11859  m1exp1  12485  bitsfzolem  12538  bitsfzo  12539  bitsinv1lem  12545  3prm  12723  prmdc  12725  pcgcd1  12924  pc2dvds  12926  pcmpt  12939  exmidunben  13070  unct  13086  fvprif  13449  blssioo  15306  pilem3  15536  perfectlem1  15752  lgsval2lem  15768  umgredgnlp  16032  clwwlkn0  16288  clwwlknnn  16292  trlsegvdegfi  16347  eupth2lem3lem4fi  16353  konigsberg  16373  bj-charfunbi  16466  bj-intexr  16563  bj-intnexr  16564  3dom  16647  2omap  16654  subctctexmid  16661  nninfsellemeq  16679  exmidsbthrlem  16689