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  7880  omopthlem2  8648  fineqv  9230  nelaneqOLD  9568  sucprcreg  9571  nd3  10585  axunndlem1  10591  axregndlem1  10598  axregndlem2  10599  axregnd  10600  axacndlem5  10607  canthp1lem2  10649  alephgch  10670  inatsk  10774  addnidpi  10897  indpi  10903  archnq  10976  fsumsplit  15810  sumsplit  15837  geoisum1c  15952  fprodm1  16039  m1dvdsndvds  16875  gexdvds  19677  chtub  27405  nolt02o  27888  nogt01o  27889  wlkp1lem6  30055  avril1  30843  ballotlemi1  34917  ballotlemii  34918  fineqvnttrclse  35553  onvf1odlem1  35603  distel  36306  onsucsuccmpi  36987  axtcond  37022  mh-setindnd  37081  bj-inftyexpitaudisj  37882  bj-inftyexpidisj  37887  poimirlem28  38332  poimirlem32  38336  n0eldmqseq  39416  lcmineqlem23  42851  nvelim  47893  0nodd  48968  2nodd  48970