Theorem mtbii 326

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

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

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 207

This theorem is referenced by:  limom  7821  omopthlem2  8584  fineqv  9162  nelaneq  9498  nd3  10491  axunndlem1  10497  axregndlem1  10504  axregndlem2  10505  axregnd  10506  axacndlem5  10513  canthp1lem2  10555  alephgch  10576  inatsk  10680  addnidpi  10803  indpi  10809  archnq  10882  fsumsplit  15655  sumsplit  15682  geoisum1c  15794  fprodm1  15881  m1dvdsndvds  16717  gexdvds  19504  chtub  27170  nolt02o  27654  nogt01o  27655  wlkp1lem6  29676  avril1  30464  ballotlemi1  34588  ballotlemii  34589  fineqvnttrclse  35216  onvf1odlem1  35219  distel  35917  onsucsuccmpi  36559  bj-inftyexpitaudisj  37322  bj-inftyexpidisj  37327  poimirlem28  37761  poimirlem32  37765  n0eldmqseq  38820  lcmineqlem23  42217  nvelim  47285  0nodd  48332  2nodd  48334