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  2329  neleqtrd  2330  eueq3dc  2991  efrirr  4474  fidcenumlemrks  7223  2omap  7269  nqnq0pi  7753  zdclt  9655  xleaddadd  10220  qdclt  10605  frec2uzf1od  10768  expnegap0  10909  bcval5  11125  zfz1isolemiso  11211  seq3coll  11214  fisumss  12078  fprodssdc  12276  nninfctlemfo  12736  rpdvds  12796  oddpwdclemodd  12869  pceq0  13020  pcmpt  13041  gsumfzval  13604  ply1termlem  15607  lgseisenlem1  15943  lgsquadlem3  15952  2sqlem8a  15995  2sqlem8  15996  pwle2  16772