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  7879  omopthlem2  8647  fineqv  9228  nelaneqOLD  9566  sucprcreg  9569  nd3  10575  axunndlem1  10581  axregndlem1  10588  axregndlem2  10589  axregnd  10590  axacndlem5  10597  canthp1lem2  10639  alephgch  10660  inatsk  10764  addnidpi  10887  indpi  10893  archnq  10966  fsumsplit  15794  sumsplit  15821  geoisum1c  15936  fprodm1  16023  m1dvdsndvds  16859  gexdvds  19655  chtub  27357  nolt02o  27840  nogt01o  27841  wlkp1lem6  30007  avril1  30795  ballotlemi1  34874  ballotlemii  34875  fineqvnttrclse  35518  onvf1odlem1  35568  distel  36274  onsucsuccmpi  36935  axtcond  36970  mh-setindnd  37029  bj-inftyexpitaudisj  37830  bj-inftyexpidisj  37835  poimirlem28  38280  poimirlem32  38284  n0eldmqseq  39364  lcmineqlem23  42799  nvelim  47843  0nodd  48918  2nodd  48920