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  7806  omopthlem2  8569  fineqv  9145  nelaneq  9481  nd3  10471  axunndlem1  10477  axregndlem1  10484  axregndlem2  10485  axregnd  10486  axacndlem5  10493  canthp1lem2  10535  alephgch  10556  inatsk  10660  addnidpi  10783  indpi  10789  archnq  10862  fsumsplit  15635  sumsplit  15662  geoisum1c  15774  fprodm1  15861  m1dvdsndvds  16697  gexdvds  19450  chtub  27104  nolt02o  27588  nogt01o  27589  wlkp1lem6  29609  avril1  30394  ballotlemi1  34484  ballotlemii  34485  fineqvnttrclse  35090  onvf1odlem1  35093  distel  35794  onsucsuccmpi  36434  bj-inftyexpitaudisj  37196  bj-inftyexpidisj  37201  poimirlem28  37645  poimirlem32  37649  n0eldmqseq  38644  lcmineqlem23  42041  nvelim  47121  0nodd  48168  2nodd  48170