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

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

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 206

This theorem is referenced by:  limom  7871  omopthlem2  8659  fineqv  9263  nd3  10584  axunndlem1  10590  axregndlem1  10597  axregndlem2  10598  axregnd  10599  axacndlem5  10606  canthp1lem2  10648  alephgch  10669  inatsk  10773  addnidpi  10896  indpi  10902  archnq  10975  fsumsplit  15687  sumsplit  15714  geoisum1c  15826  fprodm1  15911  m1dvdsndvds  16731  gexdvds  19452  chtub  26715  nolt02o  27198  nogt01o  27199  wlkp1lem6  28966  avril1  29747  ballotlemi1  33532  ballotlemii  33533  distel  34806  onsucsuccmpi  35376  bj-inftyexpitaudisj  36134  bj-inftyexpidisj  36139  poimirlem28  36564  poimirlem32  36568  n0eldmqseq  37567  lcmineqlem23  40964  nvelim  45879  0nodd  46628  2nodd  46630