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  7728  omopthlem2  8490  fineqv  9038  nd3  10345  axunndlem1  10351  axregndlem1  10358  axregndlem2  10359  axregnd  10360  axacndlem5  10367  canthp1lem2  10409  alephgch  10430  inatsk  10534  addnidpi  10657  indpi  10663  archnq  10736  fsumsplit  15453  sumsplit  15480  geoisum1c  15592  fprodm1  15677  m1dvdsndvds  16499  gexdvds  19189  chtub  26360  wlkp1lem6  28046  avril1  28827  ballotlemi1  32469  ballotlemii  32470  distel  33779  nolt02o  33898  nogt01o  33899  onsucsuccmpi  34632  bj-inftyexpitaudisj  35376  bj-inftyexpidisj  35381  poimirlem28  35805  poimirlem32  35809  n0eldmqseq  36762  lcmineqlem23  40059  nvelim  44615  0nodd  45364  2nodd  45366