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  7878  omopthlem2  8648  fineqv  9237  nelaneqOLD  9575  sucprcreg  9578  nd3  10598  axunndlem1  10604  axregndlem1  10611  axregndlem2  10612  axregnd  10613  axacndlem5  10620  canthp1lem2  10662  alephgch  10683  inatsk  10787  addnidpi  10910  indpi  10916  archnq  10989  fsumsplit  15827  sumsplit  15854  geoisum1c  15969  fprodm1  16054  m1dvdsndvds  16890  gexdvds  19711  chtub  27448  nolt02o  27931  nogt01o  27932  wlkp1lem6  30136  avril1  30943  ballotlemi1  35014  ballotlemii  35015  fineqvnttrclse  35650  onvf1odlem1  35700  distel  36380  onsucsuccmpi  37062  axtcond  37097  mh-setindnd  37156  bj-inftyexpitaudisj  37957  bj-inftyexpidisj  37962  poimirlem28  38397  poimirlem32  38401  n0eldmqseq  39482  lcmineqlem23  42917  nvelim  48011  0nodd  49085  2nodd  49087