Theorem mtbii 326

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 248	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtoi 199	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 207

This theorem is referenced by:  limom  7834  omopthlem2  8598  fineqv  9179  nelaneq  9518  nd3  10512  axunndlem1  10518  axregndlem1  10525  axregndlem2  10526  axregnd  10527  axacndlem5  10534  canthp1lem2  10576  alephgch  10597  inatsk  10701  addnidpi  10824  indpi  10830  archnq  10903  fsumsplit  15676  sumsplit  15703  geoisum1c  15815  fprodm1  15902  m1dvdsndvds  16738  gexdvds  19525  chtub  27191  nolt02o  27675  nogt01o  27676  wlkp1lem6  29762  avril1  30550  ballotlemi1  34680  ballotlemii  34681  fineqvnttrclse  35299  onvf1odlem1  35316  distel  36014  onsucsuccmpi  36656  mh-setindnd  36686  bj-inftyexpitaudisj  37457  bj-inftyexpidisj  37462  poimirlem28  37896  poimirlem32  37900  n0eldmqseq  38982  lcmineqlem23  42418  nvelim  47480  0nodd  48527  2nodd  48529