Theorem mtbii 327

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

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

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 208

This theorem is referenced by:  limom  7829  omopthlem2  8593  fineqv  9174  nelaneqOLD  9515  sucprcreg  9518  nd3  10510  axunndlem1  10516  axregndlem1  10523  axregndlem2  10524  axregnd  10525  axacndlem5  10532  canthp1lem2  10574  alephgch  10595  inatsk  10699  addnidpi  10822  indpi  10828  archnq  10901  fsumsplit  15701  sumsplit  15728  geoisum1c  15843  fprodm1  15930  m1dvdsndvds  16767  gexdvds  19557  chtub  27200  nolt02o  27684  nogt01o  27685  wlkp1lem6  29770  avril1  30558  ballotlemi1  34694  ballotlemii  34695  fineqvnttrclse  35312  onvf1odlem1  35338  distel  36036  onsucsuccmpi  36678  axtcond  36713  mh-setindnd  36772  bj-inftyexpitaudisj  37572  bj-inftyexpidisj  37577  poimirlem28  38022  poimirlem32  38026  n0eldmqseq  39108  lcmineqlem23  42543  nvelim  47593  0nodd  48668  2nodd  48670