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  7858  omopthlem2  8624  fineqv  9210  nd3  10542  axunndlem1  10548  axregndlem1  10555  axregndlem2  10556  axregnd  10557  axacndlem5  10564  canthp1lem2  10606  alephgch  10627  inatsk  10731  addnidpi  10854  indpi  10860  archnq  10933  fsumsplit  15707  sumsplit  15734  geoisum1c  15846  fprodm1  15933  m1dvdsndvds  16769  gexdvds  19514  chtub  27123  nolt02o  27607  nogt01o  27608  wlkp1lem6  29606  avril1  30392  ballotlemi1  34494  ballotlemii  34495  onvf1odlem1  35090  distel  35791  onsucsuccmpi  36431  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  poimirlem28  37642  poimirlem32  37646  n0eldmqseq  38641  lcmineqlem23  42039  nvelim  47124  0nodd  48158  2nodd  48160