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 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  limom  7874  omopthlem2  8642  fineqv  9223  nelaneqOLD  9561  sucprcreg  9564  nd3  10570  axunndlem1  10576  axregndlem1  10583  axregndlem2  10584  axregnd  10585  axacndlem5  10592  canthp1lem2  10634  alephgch  10655  inatsk  10759  addnidpi  10882  indpi  10888  archnq  10961  fsumsplit  15788  sumsplit  15815  geoisum1c  15930  fprodm1  16017  m1dvdsndvds  16854  gexdvds  19650  chtub  27338  nolt02o  27821  nogt01o  27822  wlkp1lem6  29963  avril1  30751  ballotlemi1  34834  ballotlemii  34835  fineqvnttrclse  35456  onvf1odlem1  35482  distel  36188  onsucsuccmpi  36839  axtcond  36874  mh-setindnd  36933  bj-inftyexpitaudisj  37732  bj-inftyexpidisj  37737  poimirlem28  38182  poimirlem32  38186  n0eldmqseq  39268  lcmineqlem23  42703  nvelim  47742  0nodd  48817  2nodd  48819