Theorem mtbii 329

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 251	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtoi 202	1 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  nvelim  5280  limom  7927  omopthlem2  8707  fineqv  9296  nelaneqOLD  9634  sucprcreg  9637  nd3  10713  axunndlem1  10719  axregndlem1  10726  axregndlem2  10727  axregnd  10728  axacndlem5  10735  canthp1lem2  10777  alephgch  10798  inatsk  10902  addnidpi  11025  indpi  11031  archnq  11104  fsumsplit  15951  sumsplit  15978  geoisum1c  16093  fprodm1  16178  m1dvdsndvds  17020  gexdvds  19849  chtub  27596  nolt02o  28109  nogt01o  28110  wlkp1lem6  30314  avril1  31121  ballotlemi1  35246  ballotlemii  35247  fineqvnttrclse  35933  onvf1odlem1  36072  distel  36780  onsucsuccmpi  37446  axtcond  37481  mh-setindnd  37540  bj-inftyexpitaudisj  38394  bj-inftyexpidisj  38399  poimirlem28  38834  poimirlem32  38838  n0eldmqseq  39932  lcmineqlem23  43367  0nodd  49540  2nodd  49542