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  7824  omopthlem2  8588  fineqv  9167  nelaneq  9506  nd3  10500  axunndlem1  10506  axregndlem1  10513  axregndlem2  10514  axregnd  10515  axacndlem5  10522  canthp1lem2  10564  alephgch  10585  inatsk  10689  addnidpi  10812  indpi  10818  archnq  10891  fsumsplit  15664  sumsplit  15691  geoisum1c  15803  fprodm1  15890  m1dvdsndvds  16726  gexdvds  19513  chtub  27179  nolt02o  27663  nogt01o  27664  wlkp1lem6  29750  avril1  30538  ballotlemi1  34660  ballotlemii  34661  fineqvnttrclse  35280  onvf1odlem1  35297  distel  35995  onsucsuccmpi  36637  mh-setindnd  36667  bj-inftyexpitaudisj  37410  bj-inftyexpidisj  37415  poimirlem28  37849  poimirlem32  37853  n0eldmqseq  38908  lcmineqlem23  42305  nvelim  47369  0nodd  48416  2nodd  48418