Theorem mtbii 328

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

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

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 209

This theorem is referenced by:  limom  7597  omopthlem2  8285  fineqv  8735  nd3  10013  axunndlem1  10019  axregndlem1  10026  axregndlem2  10027  axregnd  10028  axacndlem5  10035  canthp1lem2  10077  alephgch  10098  inatsk  10202  addnidpi  10325  indpi  10331  archnq  10404  fsumsplit  15099  sumsplit  15125  geoisum1c  15238  fprodm1  15323  m1dvdsndvds  16137  gexdvds  18711  chtub  25790  wlkp1lem6  27462  avril1  28244  ballotlemi1  31762  ballotlemii  31763  distel  33050  nolt02o  33201  onsucsuccmpi  33793  bj-inftyexpitaudisj  34489  bj-inftyexpidisj  34494  poimirlem28  34922  poimirlem32  34926  n0eldmqseq  35886  nvelim  43329  0nodd  44084  2nodd  44086