Theorem mtbiri 676

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 665	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3452  n0i  3453  axnul  4155  intexr  4180  intnexr  4181  iin0r  4199  exmid01  4228  ordtriexmidlem  4552  ordtriexmidlem2  4553  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  sucprcreg  4582  preleq  4588  reg3exmidlemwe  4612  dcextest  4614  nn0eln0  4653  0nelelxp  4689  canth  5872  tfrlemisucaccv  6380  nnsucuniel  6550  nndceq  6554  nndcel  6555  2dom  6861  snnen2oprc  6918  snexxph  7011  elfi2  7033  djune  7139  updjudhcoinrg  7142  omp1eomlem  7155  nnnninfeq  7189  ismkvnex  7216  mkvprop  7219  omniwomnimkv  7228  nninfwlpoimlemginf  7237  exmidfodomrlemrALT  7265  exmidaclem  7270  netap  7316  2omotaplemap  7319  elni2  7376  ltsopi  7382  ltsonq  7460  renepnf  8069  renemnf  8070  lt0ne0d  8534  sup3exmid  8978  nnne0  9012  nn0ge2m1nn  9303  nn0nepnf  9314  xrltnr  9848  pnfnlt  9856  nltmnf  9857  xrltnsym  9862  xrlttri3  9866  nltpnft  9883  ngtmnft  9886  xrrebnd  9888  xrpnfdc  9911  xrmnfdc  9912  xsubge0  9950  xposdif  9951  xleaddadd  9956  fzpreddisj  10140  fzm1  10169  exfzdc  10310  xnn0nnen  10511  xrbdtri  11422  m1exp1  12045  3prm  12269  prmdc  12271  pcgcd1  12469  pc2dvds  12471  pcmpt  12484  exmidunben  12586  unct  12602  fvprif  12929  blssioo  14732  pilem3  14959  lgsval2lem  15167  bj-charfunbi  15373  bj-intexr  15470  bj-intnexr  15471  subctctexmid  15561  nninfsellemeq  15574  exmidsbthrlem  15582