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  7807  omopthlem2  8570  fineqv  9146  nelaneq  9482  nd3  10475  axunndlem1  10481  axregndlem1  10488  axregndlem2  10489  axregnd  10490  axacndlem5  10497  canthp1lem2  10539  alephgch  10560  inatsk  10664  addnidpi  10787  indpi  10793  archnq  10866  fsumsplit  15643  sumsplit  15670  geoisum1c  15782  fprodm1  15869  m1dvdsndvds  16705  gexdvds  19491  chtub  27145  nolt02o  27629  nogt01o  27630  wlkp1lem6  29650  avril1  30435  ballotlemi1  34508  ballotlemii  34509  fineqvnttrclse  35136  onvf1odlem1  35139  distel  35837  onsucsuccmpi  36477  bj-inftyexpitaudisj  37239  bj-inftyexpidisj  37244  poimirlem28  37688  poimirlem32  37692  n0eldmqseq  38687  lcmineqlem23  42084  nvelim  47154  0nodd  48201  2nodd  48203