Theorem mtbid 674

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 665	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  678  eqneltrrd  2302  neleqtrd  2303  eueq3dc  2947  efrirr  4401  fidcenumlemrks  7057  nqnq0pi  7553  zdclt  9452  xleaddadd  10011  qdclt  10390  frec2uzf1od  10553  expnegap0  10694  bcval5  10910  zfz1isolemiso  10986  seq3coll  10989  fisumss  11736  fprodssdc  11934  nninfctlemfo  12394  rpdvds  12454  oddpwdclemodd  12527  pceq0  12678  pcmpt  12699  gsumfzval  13256  ply1termlem  15247  lgseisenlem1  15580  lgsquadlem3  15589  2sqlem8a  15632  2sqlem8  15633  2omap  15969  pwle2  15972