Theorem mtbiri 675

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 664	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3427  n0i  3428  axnul  4128  intexr  4150  intnexr  4151  iin0r  4169  exmid01  4198  ordtriexmidlem  4518  ordtriexmidlem2  4519  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  sucprcreg  4548  preleq  4554  reg3exmidlemwe  4578  dcextest  4580  nn0eln0  4619  0nelelxp  4655  canth  5828  tfrlemisucaccv  6325  nnsucuniel  6495  nndceq  6499  nndcel  6500  2dom  6804  snnen2oprc  6859  snexxph  6948  elfi2  6970  djune  7076  updjudhcoinrg  7079  omp1eomlem  7092  nnnninfeq  7125  ismkvnex  7152  mkvprop  7155  omniwomnimkv  7164  nninfwlpoimlemginf  7173  exmidfodomrlemrALT  7201  exmidaclem  7206  netap  7252  2omotaplemap  7255  elni2  7312  ltsopi  7318  ltsonq  7396  renepnf  8004  renemnf  8005  lt0ne0d  8469  sup3exmid  8913  nnne0  8946  nn0ge2m1nn  9235  nn0nepnf  9246  xrltnr  9778  pnfnlt  9786  nltmnf  9787  xrltnsym  9792  xrlttri3  9796  nltpnft  9813  ngtmnft  9816  xrrebnd  9818  xrpnfdc  9841  xrmnfdc  9842  xsubge0  9880  xposdif  9881  xleaddadd  9886  fzpreddisj  10070  fzm1  10099  exfzdc  10239  xrbdtri  11283  m1exp1  11905  3prm  12127  prmdc  12129  pcgcd1  12326  pc2dvds  12328  pcmpt  12340  exmidunben  12426  unct  12442  fvprif  12761  blssioo  14015  pilem3  14174  lgsval2lem  14381  bj-charfunbi  14533  bj-intexr  14630  bj-intnexr  14631  subctctexmid  14720  nninfsellemeq  14733  exmidsbthrlem  14740