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  7870  omopthlem2  8658  fineqv  9262  nd3  10583  axunndlem1  10589  axregndlem1  10596  axregndlem2  10597  axregnd  10598  axacndlem5  10605  canthp1lem2  10647  alephgch  10668  inatsk  10772  addnidpi  10895  indpi  10901  archnq  10974  fsumsplit  15686  sumsplit  15713  geoisum1c  15825  fprodm1  15910  m1dvdsndvds  16730  gexdvds  19451  chtub  26712  nolt02o  27195  nogt01o  27196  wlkp1lem6  28932  avril1  29713  ballotlemi1  33496  ballotlemii  33497  distel  34770  onsucsuccmpi  35323  bj-inftyexpitaudisj  36081  bj-inftyexpidisj  36086  poimirlem28  36511  poimirlem32  36515  n0eldmqseq  37514  lcmineqlem23  40911  nvelim  45821  0nodd  46570  2nodd  46572