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  7919  omopthlem2  8716  fineqv  9326  nd3  10658  axunndlem1  10664  axregndlem1  10671  axregndlem2  10672  axregnd  10673  axacndlem5  10680  canthp1lem2  10722  alephgch  10743  inatsk  10847  addnidpi  10970  indpi  10976  archnq  11049  fsumsplit  15789  sumsplit  15816  geoisum1c  15928  fprodm1  16015  m1dvdsndvds  16845  gexdvds  19626  chtub  27274  nolt02o  27758  nogt01o  27759  wlkp1lem6  29714  avril1  30495  ballotlemi1  34467  ballotlemii  34468  distel  35767  onsucsuccmpi  36409  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  poimirlem28  37608  poimirlem32  37612  n0eldmqseq  38605  lcmineqlem23  42008  nvelim  47038  0nodd  47893  2nodd  47895