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:  limom  7894  omopthlem2  8673  fineqv  9262  nelaneqOLD  9601  sucprcreg  9604  nd3  10678  axunndlem1  10684  axregndlem1  10691  axregndlem2  10692  axregnd  10693  axacndlem5  10700  canthp1lem2  10742  alephgch  10763  inatsk  10867  addnidpi  10990  indpi  10996  archnq  11069  fsumsplit  15913  sumsplit  15940  geoisum1c  16055  fprodm1  16140  m1dvdsndvds  16982  gexdvds  19804  chtub  27545  nolt02o  28058  nogt01o  28059  wlkp1lem6  30263  avril1  31070  ballotlemi1  35182  ballotlemii  35183  fineqvnttrclse  35849  onvf1odlem1  35951  distel  36658  onsucsuccmpi  37324  axtcond  37359  mh-setindnd  37418  bj-inftyexpitaudisj  38220  bj-inftyexpidisj  38225  poimirlem28  38660  poimirlem32  38664  n0eldmqseq  39760  lcmineqlem23  43195  nvelim  48287  0nodd  49361  2nodd  49363