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  2304  neleqtrd  2305  eueq3dc  2954  efrirr  4418  fidcenumlemrks  7081  nqnq0pi  7586  zdclt  9485  xleaddadd  10044  qdclt  10425  frec2uzf1od  10588  expnegap0  10729  bcval5  10945  zfz1isolemiso  11021  seq3coll  11024  fisumss  11818  fprodssdc  12016  nninfctlemfo  12476  rpdvds  12536  oddpwdclemodd  12609  pceq0  12760  pcmpt  12781  gsumfzval  13338  ply1termlem  15329  lgseisenlem1  15662  lgsquadlem3  15671  2sqlem8a  15714  2sqlem8  15715  2omap  16132  pwle2  16137