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  7904  omopthlem2  8699  fineqv  9300  nd3  10630  axunndlem1  10636  axregndlem1  10643  axregndlem2  10644  axregnd  10645  axacndlem5  10652  canthp1lem2  10694  alephgch  10715  inatsk  10819  addnidpi  10942  indpi  10948  archnq  11021  fsumsplit  15778  sumsplit  15805  geoisum1c  15917  fprodm1  16004  m1dvdsndvds  16837  gexdvds  19603  chtub  27257  nolt02o  27741  nogt01o  27742  wlkp1lem6  29697  avril1  30483  ballotlemi1  34506  ballotlemii  34507  distel  35805  onsucsuccmpi  36445  bj-inftyexpitaudisj  37207  bj-inftyexpidisj  37212  poimirlem28  37656  poimirlem32  37660  n0eldmqseq  38651  lcmineqlem23  42053  nvelim  47140  0nodd  48091  2nodd  48093