Theorem mtbii 329

Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)

Hypotheses

Ref	Expression
mtbii.min	⊢ ¬ 𝜓
mtbii.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbii	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem mtbii

Step	Hyp	Ref	Expression
1		mtbii.min	. 2 ⊢ ¬ 𝜓
2		mtbii.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 251	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtoi 202	1 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  limom  7876  omopthlem2  8644  fineqv  9225  nelaneqOLD  9563  sucprcreg  9566  nd3  10580  axunndlem1  10586  axregndlem1  10593  axregndlem2  10594  axregnd  10595  axacndlem5  10602  canthp1lem2  10644  alephgch  10665  inatsk  10769  addnidpi  10892  indpi  10898  archnq  10971  fsumsplit  15799  sumsplit  15826  geoisum1c  15941  fprodm1  16028  m1dvdsndvds  16864  gexdvds  19660  chtub  27387  nolt02o  27870  nogt01o  27871  wlkp1lem6  30037  avril1  30825  ballotlemi1  34902  ballotlemii  34903  fineqvnttrclse  35545  onvf1odlem1  35595  distel  36301  onsucsuccmpi  36982  axtcond  37017  mh-setindnd  37076  bj-inftyexpitaudisj  37877  bj-inftyexpidisj  37882  poimirlem28  38327  poimirlem32  38331  n0eldmqseq  39411  lcmineqlem23  42846  nvelim  47888  0nodd  48963  2nodd  48965