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  7796  omopthlem2  8561  fineqv  9128  nd3  10446  axunndlem1  10452  axregndlem1  10459  axregndlem2  10460  axregnd  10461  axacndlem5  10468  canthp1lem2  10510  alephgch  10531  inatsk  10635  addnidpi  10758  indpi  10764  archnq  10837  fsumsplit  15552  sumsplit  15579  geoisum1c  15691  fprodm1  15776  m1dvdsndvds  16596  gexdvds  19285  chtub  26466  nolt02o  26949  nogt01o  26950  wlkp1lem6  28334  avril1  29115  ballotlemi1  32769  ballotlemii  32770  distel  34062  onsucsuccmpi  34728  bj-inftyexpitaudisj  35481  bj-inftyexpidisj  35486  poimirlem28  35910  poimirlem32  35914  n0eldmqseq  36916  lcmineqlem23  40313  nvelim  44966  0nodd  45715  2nodd  45717