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  7822  omopthlem2  8585  fineqv  9168  nelaneq  9512  nd3  10502  axunndlem1  10508  axregndlem1  10515  axregndlem2  10516  axregnd  10517  axacndlem5  10524  canthp1lem2  10566  alephgch  10587  inatsk  10691  addnidpi  10814  indpi  10820  archnq  10893  fsumsplit  15666  sumsplit  15693  geoisum1c  15805  fprodm1  15892  m1dvdsndvds  16728  gexdvds  19481  chtub  27139  nolt02o  27623  nogt01o  27624  wlkp1lem6  29640  avril1  30425  ballotlemi1  34473  ballotlemii  34474  onvf1odlem1  35078  distel  35779  onsucsuccmpi  36419  bj-inftyexpitaudisj  37181  bj-inftyexpidisj  37186  poimirlem28  37630  poimirlem32  37634  n0eldmqseq  38629  lcmineqlem23  42027  nvelim  47111  0nodd  48158  2nodd  48160