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  7838  omopthlem2  8601  fineqv  9186  nd3  10518  axunndlem1  10524  axregndlem1  10531  axregndlem2  10532  axregnd  10533  axacndlem5  10540  canthp1lem2  10582  alephgch  10603  inatsk  10707  addnidpi  10830  indpi  10836  archnq  10909  fsumsplit  15683  sumsplit  15710  geoisum1c  15822  fprodm1  15909  m1dvdsndvds  16745  gexdvds  19490  chtub  27099  nolt02o  27583  nogt01o  27584  wlkp1lem6  29580  avril1  30365  ballotlemi1  34467  ballotlemii  34468  onvf1odlem1  35063  distel  35764  onsucsuccmpi  36404  bj-inftyexpitaudisj  37166  bj-inftyexpidisj  37171  poimirlem28  37615  poimirlem32  37619  n0eldmqseq  38614  lcmineqlem23  42012  nvelim  47097  0nodd  48131  2nodd  48133