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  7589  omopthlem2  8277  fineqv  8727  nd3  10005  axunndlem1  10011  axregndlem1  10018  axregndlem2  10019  axregnd  10020  axacndlem5  10027  canthp1lem2  10069  alephgch  10090  inatsk  10194  addnidpi  10317  indpi  10323  archnq  10396  fsumsplit  15091  sumsplit  15117  geoisum1c  15230  fprodm1  15315  m1dvdsndvds  16129  gexdvds  18703  chtub  25782  wlkp1lem6  27454  avril1  28236  ballotlemi1  31755  ballotlemii  31756  distel  33043  nolt02o  33194  onsucsuccmpi  33786  bj-inftyexpitaudisj  34481  bj-inftyexpidisj  34486  poimirlem28  34914  poimirlem32  34918  n0eldmqseq  35878  nvelim  43316  0nodd  44071  2nodd  44073