Theorem mtbii 328

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

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

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 209

This theorem is referenced by:  limom  7857  omopthlem2  8624  fineqv  9205  nelaneqOLD  9545  sucprcreg  9548  nd3  10541  axunndlem1  10547  axregndlem1  10554  axregndlem2  10555  axregnd  10556  axacndlem5  10563  canthp1lem2  10605  alephgch  10626  inatsk  10730  addnidpi  10853  indpi  10859  archnq  10932  fsumsplit  15759  sumsplit  15786  geoisum1c  15901  fprodm1  15988  m1dvdsndvds  16825  gexdvds  19615  chtub  27264  nolt02o  27747  nogt01o  27748  wlkp1lem6  29834  avril1  30622  ballotlemi1  34761  ballotlemii  34762  fineqvnttrclse  35381  onvf1odlem1  35407  distel  36112  onsucsuccmpi  36764  axtcond  36799  mh-setindnd  36858  bj-inftyexpitaudisj  37658  bj-inftyexpidisj  37663  poimirlem28  38108  poimirlem32  38112  n0eldmqseq  39194  lcmineqlem23  42629  nvelim  47678  0nodd  48753  2nodd  48755