Theorem mtbii 326

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 248	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtoi 199	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  limom  7833  omopthlem2  8596  fineqv  9177  nelaneqOLD  9517  sucprcreg  9520  nd3  10512  axunndlem1  10518  axregndlem1  10525  axregndlem2  10526  axregnd  10527  axacndlem5  10534  canthp1lem2  10576  alephgch  10597  inatsk  10701  addnidpi  10824  indpi  10830  archnq  10903  fsumsplit  15703  sumsplit  15730  geoisum1c  15845  fprodm1  15932  m1dvdsndvds  16769  gexdvds  19559  chtub  27175  nolt02o  27659  nogt01o  27660  wlkp1lem6  29745  avril1  30533  ballotlemi1  34647  ballotlemii  34648  fineqvnttrclse  35268  onvf1odlem1  35285  distel  35983  onsucsuccmpi  36625  axtcond  36660  mh-setindnd  36719  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  poimirlem28  37969  poimirlem32  37973  n0eldmqseq  39055  lcmineqlem23  42490  nvelim  47571  0nodd  48646  2nodd  48648