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  2328  neleqtrd  2329  eueq3dc  2981  efrirr  4456  fidcenumlemrks  7195  nqnq0pi  7718  zdclt  9618  xleaddadd  10183  qdclt  10568  frec2uzf1od  10731  expnegap0  10872  bcval5  11088  zfz1isolemiso  11166  seq3coll  11169  fisumss  12033  fprodssdc  12231  nninfctlemfo  12691  rpdvds  12751  oddpwdclemodd  12824  pceq0  12975  pcmpt  12996  gsumfzval  13554  ply1termlem  15553  lgseisenlem1  15889  lgsquadlem3  15898  2sqlem8a  15941  2sqlem8  15942  2omap  16715  pwle2  16720