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  3515  n0i  3516  axnul  4237  intexr  4264  intnexr  4265  iin0r  4284  exmid01  4313  ordtriexmidlem  4643  ordtriexmidlem2  4644  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  sucprcreg  4673  preleq  4679  reg3exmidlemwe  4703  dcextest  4705  nn0eln0  4744  0nelelxp  4780  canth  6003  tfrlemisucaccv  6558  nnsucuniel  6730  nndceq  6734  nndcel  6735  2dom  7048  snnen2oprc  7116  snexxph  7222  elfi2  7261  2omap  7271  djune  7371  updjudhcoinrg  7374  omp1eomlem  7387  nnnninfeq  7421  ismkvnex  7448  mkvprop  7451  omniwomnimkv  7460  nninfwlpoimlemginf  7469  exmidfodomrlemrALT  7508  exmidaclem  7517  netap  7573  2omotaplemap  7576  elni2  7634  ltsopi  7640  ltsonq  7718  renepnf  8326  renemnf  8327  lt0ne0d  8792  sup3exmid  9236  nnne0  9270  nn0ge2m1nn  9565  nn0nepnf  9576  xrltnr  10118  pnfnlt  10126  nltmnf  10127  xrltnsym  10132  xrlttri3  10136  nltpnft  10153  ngtmnft  10156  xrrebnd  10158  xrpnfdc  10181  xrmnfdc  10182  xsubge0  10220  xposdif  10221  xleaddadd  10226  fzpreddisj  10412  fzm1  10441  exfzdc  10593  xnn0nnen  10806  hashtpglem  11226  lsw0  11280  cats1un  11421  xrbdtri  11969  m1exp1  12595  bitsfzolem  12648  bitsfzo  12649  bitsinv1lem  12655  3prm  12833  prmdc  12835  pcgcd1  13034  pc2dvds  13036  pcmpt  13049  ballotfilem4  13163  exmidunben  13198  unct  13214  fvprif  13577  blssioo  15467  pilem3  15697  perfectlem1  15916  lgsval2lem  15932  umgredgnlp  16196  clwwlkn0  16452  clwwlknnn  16456  trlsegvdegfi  16511  eupth2lem3lem4fi  16517  konigsberg  16537  bj-charfunbi  16630  bj-intexr  16727  bj-intnexr  16728  3dom  16811  subctctexmid  16823  nninfsellemeq  16841  exmidsbthrlem  16851