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  7882  omopthlem2  8677  fineqv  9276  nd3  10608  axunndlem1  10614  axregndlem1  10621  axregndlem2  10622  axregnd  10623  axacndlem5  10630  canthp1lem2  10672  alephgch  10693  inatsk  10797  addnidpi  10920  indpi  10926  archnq  10999  fsumsplit  15762  sumsplit  15789  geoisum1c  15901  fprodm1  15988  m1dvdsndvds  16823  gexdvds  19570  chtub  27180  nolt02o  27664  nogt01o  27665  wlkp1lem6  29663  avril1  30449  ballotlemi1  34540  ballotlemii  34541  distel  35826  onsucsuccmpi  36466  bj-inftyexpitaudisj  37228  bj-inftyexpidisj  37233  poimirlem28  37677  poimirlem32  37681  n0eldmqseq  38672  lcmineqlem23  42069  nvelim  47119  0nodd  48112  2nodd  48114