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

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

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 206

This theorem is referenced by:  limom  7871  omopthlem2  8659  fineqv  9263  nd3  10584  axunndlem1  10590  axregndlem1  10597  axregndlem2  10598  axregnd  10599  axacndlem5  10606  canthp1lem2  10648  alephgch  10669  inatsk  10773  addnidpi  10896  indpi  10902  archnq  10975  fsumsplit  15687  sumsplit  15714  geoisum1c  15826  fprodm1  15911  m1dvdsndvds  16731  gexdvds  19452  chtub  26715  nolt02o  27198  nogt01o  27199  wlkp1lem6  28935  avril1  29716  ballotlemi1  33501  ballotlemii  33502  distel  34775  onsucsuccmpi  35328  bj-inftyexpitaudisj  36086  bj-inftyexpidisj  36091  poimirlem28  36516  poimirlem32  36520  n0eldmqseq  37519  lcmineqlem23  40916  nvelim  45831  0nodd  46580  2nodd  46582