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  7826  omopthlem2  8589  fineqv  9170  nelaneq  9509  nd3  10503  axunndlem1  10509  axregndlem1  10516  axregndlem2  10517  axregnd  10518  axacndlem5  10525  canthp1lem2  10567  alephgch  10588  inatsk  10692  addnidpi  10815  indpi  10821  archnq  10894  fsumsplit  15694  sumsplit  15721  geoisum1c  15836  fprodm1  15923  m1dvdsndvds  16760  gexdvds  19550  chtub  27189  nolt02o  27673  nogt01o  27674  wlkp1lem6  29760  avril1  30548  ballotlemi1  34663  ballotlemii  34664  fineqvnttrclse  35284  onvf1odlem1  35301  distel  35999  onsucsuccmpi  36641  axtcond  36676  mh-setindnd  36735  bj-inftyexpitaudisj  37535  bj-inftyexpidisj  37540  poimirlem28  37983  poimirlem32  37987  n0eldmqseq  39069  lcmineqlem23  42504  nvelim  47583  0nodd  48658  2nodd  48660