Theorem mtbii 318

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

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

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 199

This theorem is referenced by:  limom  7312  omopthlem2  7974  fineqv  8415  dfac2OLD  9239  nd3  9697  axunndlem1  9703  axregndlem1  9710  axregndlem2  9711  axregnd  9712  axacndlem5  9719  canthp1lem2  9761  alephgch  9782  inatsk  9886  addnidpi  10009  indpi  10015  archnq  10088  fsumsplit  14809  sumsplit  14835  geoisum1c  14946  fprodm1  15031  m1dvdsndvds  15833  gexdvds  18309  chtub  25286  wlkp1lem6  26923  avril1  27839  ballotlemi1  31073  ballotlemii  31074  distel  32213  nolt02o  32350  onsucsuccmpi  32942  bj-inftyexpidisj  33588  poimirlem28  33918  poimirlem32  33922  nvelim  41965  0nodd  42597  2nodd  42599