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 ⊢ (𝜑 → ¬ 𝜒)

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

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 210

This theorem is referenced by:  limom  7575  omopthlem2  8266  fineqv  8717  nd3  10000  axunndlem1  10006  axregndlem1  10013  axregndlem2  10014  axregnd  10015  axacndlem5  10022  canthp1lem2  10064  alephgch  10085  inatsk  10189  addnidpi  10312  indpi  10318  archnq  10391  fsumsplit  15089  sumsplit  15115  geoisum1c  15228  fprodm1  15313  m1dvdsndvds  16125  gexdvds  18701  chtub  25796  wlkp1lem6  27468  avril1  28248  ballotlemi1  31870  ballotlemii  31871  distel  33161  nolt02o  33312  onsucsuccmpi  33904  bj-inftyexpitaudisj  34620  bj-inftyexpidisj  34625  poimirlem28  35085  poimirlem32  35089  n0eldmqseq  36044  lcmineqlem23  39339  nvelim  43679  0nodd  44430  2nodd  44432