Theorem mtbii 325

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  7884  omopthlem2  8682  fineqv  9290  nd3  10623  axunndlem1  10629  axregndlem1  10636  axregndlem2  10637  axregnd  10638  axacndlem5  10645  canthp1lem2  10687  alephgch  10708  inatsk  10812  addnidpi  10935  indpi  10941  archnq  11014  fsumsplit  15740  sumsplit  15767  geoisum1c  15879  fprodm1  15964  m1dvdsndvds  16795  gexdvds  19578  chtub  27238  nolt02o  27722  nogt01o  27723  wlkp1lem6  29612  avril1  30393  ballotlemi1  34349  ballotlemii  34350  distel  35640  onsucsuccmpi  36168  bj-inftyexpitaudisj  36925  bj-inftyexpidisj  36930  poimirlem28  37362  poimirlem32  37366  n0eldmqseq  38360  lcmineqlem23  41763  nvelim  46772  0nodd  47583  2nodd  47585