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  3428  n0i  3429  axnul  4129  intexr  4151  intnexr  4152  iin0r  4170  exmid01  4199  ordtriexmidlem  4519  ordtriexmidlem2  4520  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  sucprcreg  4549  preleq  4555  reg3exmidlemwe  4579  dcextest  4581  nn0eln0  4620  0nelelxp  4656  canth  5829  tfrlemisucaccv  6326  nnsucuniel  6496  nndceq  6500  nndcel  6501  2dom  6805  snnen2oprc  6860  snexxph  6949  elfi2  6971  djune  7077  updjudhcoinrg  7080  omp1eomlem  7093  nnnninfeq  7126  ismkvnex  7153  mkvprop  7156  omniwomnimkv  7165  nninfwlpoimlemginf  7174  exmidfodomrlemrALT  7202  exmidaclem  7207  netap  7253  2omotaplemap  7256  elni2  7313  ltsopi  7319  ltsonq  7397  renepnf  8005  renemnf  8006  lt0ne0d  8470  sup3exmid  8914  nnne0  8947  nn0ge2m1nn  9236  nn0nepnf  9247  xrltnr  9779  pnfnlt  9787  nltmnf  9788  xrltnsym  9793  xrlttri3  9797  nltpnft  9814  ngtmnft  9817  xrrebnd  9819  xrpnfdc  9842  xrmnfdc  9843  xsubge0  9881  xposdif  9882  xleaddadd  9887  fzpreddisj  10071  fzm1  10100  exfzdc  10240  xrbdtri  11284  m1exp1  11906  3prm  12128  prmdc  12130  pcgcd1  12327  pc2dvds  12329  pcmpt  12341  exmidunben  12427  unct  12443  fvprif  12762  blssioo  14048  pilem3  14207  lgsval2lem  14414  bj-charfunbi  14566  bj-intexr  14663  bj-intnexr  14664  subctctexmid  14753  nninfsellemeq  14766  exmidsbthrlem  14773