Theorem mtbii 316

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

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

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 197

This theorem is referenced by:  limom  7080  omopthlem2  7736  fineqv  8175  dfac2  8953  nd3  9411  axunndlem1  9417  axregndlem1  9424  axregndlem2  9425  axregnd  9426  axacndlem5  9433  canthp1lem2  9475  alephgch  9496  inatsk  9600  addnidpi  9723  indpi  9729  archnq  9802  fsumsplit  14471  sumsplit  14499  geoisum1c  14611  fprodm1  14697  m1dvdsndvds  15503  gexdvds  17999  chtub  24937  wlkp1lem6  26575  avril1  27319  ballotlemi1  30564  ballotlemii  30565  distel  31709  nolt02o  31845  onsucsuccmpi  32442  bj-inftyexpidisj  33097  poimirlem28  33437  poimirlem32  33441  nvelim  41200  0nodd  41810  2nodd  41812