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  7861  omopthlem2  8627  fineqv  9217  nd3  10549  axunndlem1  10555  axregndlem1  10562  axregndlem2  10563  axregnd  10564  axacndlem5  10571  canthp1lem2  10613  alephgch  10634  inatsk  10738  addnidpi  10861  indpi  10867  archnq  10940  fsumsplit  15714  sumsplit  15741  geoisum1c  15853  fprodm1  15940  m1dvdsndvds  16776  gexdvds  19521  chtub  27130  nolt02o  27614  nogt01o  27615  wlkp1lem6  29613  avril1  30399  ballotlemi1  34501  ballotlemii  34502  onvf1odlem1  35097  distel  35798  onsucsuccmpi  36438  bj-inftyexpitaudisj  37200  bj-inftyexpidisj  37205  poimirlem28  37649  poimirlem32  37653  n0eldmqseq  38648  lcmineqlem23  42046  nvelim  47128  0nodd  48162  2nodd  48164