Theorem mtbii 329

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  limom  7891  omopthlem2  8662  fineqv  9251  nelaneqOLD  9590  sucprcreg  9593  nd3  10667  axunndlem1  10673  axregndlem1  10680  axregndlem2  10681  axregnd  10682  axacndlem5  10689  canthp1lem2  10731  alephgch  10752  inatsk  10856  addnidpi  10979  indpi  10985  archnq  11058  fsumsplit  15900  sumsplit  15927  geoisum1c  16042  fprodm1  16127  m1dvdsndvds  16969  gexdvds  19791  chtub  27532  nolt02o  28045  nogt01o  28046  wlkp1lem6  30250  avril1  31057  ballotlemi1  35128  ballotlemii  35129  fineqvnttrclse  35775  onvf1odlem1  35865  distel  36545  onsucsuccmpi  37211  axtcond  37246  mh-setindnd  37305  bj-inftyexpitaudisj  38106  bj-inftyexpidisj  38111  poimirlem28  38546  poimirlem32  38550  n0eldmqseq  39646  lcmineqlem23  43081  nvelim  48162  0nodd  49236  2nodd  49238