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

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

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 207

This theorem is referenced by:  limom  7903  omopthlem2  8697  fineqv  9297  nd3  10627  axunndlem1  10633  axregndlem1  10640  axregndlem2  10641  axregnd  10642  axacndlem5  10649  canthp1lem2  10691  alephgch  10712  inatsk  10816  addnidpi  10939  indpi  10945  archnq  11018  fsumsplit  15774  sumsplit  15801  geoisum1c  15913  fprodm1  16000  m1dvdsndvds  16832  gexdvds  19617  chtub  27271  nolt02o  27755  nogt01o  27756  wlkp1lem6  29711  avril1  30492  ballotlemi1  34484  ballotlemii  34485  distel  35785  onsucsuccmpi  36426  bj-inftyexpitaudisj  37188  bj-inftyexpidisj  37193  poimirlem28  37635  poimirlem32  37639  n0eldmqseq  38631  lcmineqlem23  42033  nvelim  47073  0nodd  48014  2nodd  48016