Theorem mtbii 325

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  7703  omopthlem2  8450  fineqv  8967  nd3  10276  axunndlem1  10282  axregndlem1  10289  axregndlem2  10290  axregnd  10291  axacndlem5  10298  canthp1lem2  10340  alephgch  10361  inatsk  10465  addnidpi  10588  indpi  10594  archnq  10667  fsumsplit  15381  sumsplit  15408  geoisum1c  15520  fprodm1  15605  m1dvdsndvds  16427  gexdvds  19104  chtub  26265  wlkp1lem6  27948  avril1  28728  ballotlemi1  32369  ballotlemii  32370  distel  33685  nolt02o  33825  nogt01o  33826  onsucsuccmpi  34559  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  poimirlem28  35732  poimirlem32  35736  n0eldmqseq  36689  lcmineqlem23  39987  nvelim  44502  0nodd  45252  2nodd  45254