Theorem mtbid 679

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

Ref	Expression
mtbid.min	⊢ (𝜑 → ¬ 𝜓)
mtbid.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbid	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		mtbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 158	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 669	1 ⊢ (𝜑 → ¬ 𝜒)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  683  eqneltrrd  2331  neleqtrd  2332  eueq3dc  2993  efrirr  4476  fidcenumlemrks  7225  2omap  7271  nqnq0pi  7755  zdclt  9657  xleaddadd  10223  qdclt  10609  frec2uzf1od  10772  expnegap0  10913  bcval5  11129  zfz1isolemiso  11215  seq3coll  11218  fisumss  12082  fprodssdc  12280  nninfctlemfo  12740  rpdvds  12800  oddpwdclemodd  12873  pceq0  13024  pcmpt  13045  gsumfzval  13621  ply1termlem  15624  lgseisenlem1  15960  lgsquadlem3  15969  2sqlem8a  16012  2sqlem8  16013  pwle2  16789