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  15667  sumsplit  15694  geoisum1c  15806  fprodm1  15893  m1dvdsndvds  16729  gexdvds  19482  chtub  27140  nolt02o  27624  nogt01o  27625  wlkp1lem6  29641  avril1  30426  ballotlemi1  34490  ballotlemii  34491  onvf1odlem1  35095  distel  35796  onsucsuccmpi  36436  bj-inftyexpitaudisj  37198  bj-inftyexpidisj  37203  poimirlem28  37647  poimirlem32  37651  n0eldmqseq  38646  lcmineqlem23  42044  nvelim  47127  0nodd  48174  2nodd  48176