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  4400  fidcenumlemrks  7055  nqnq0pi  7551  zdclt  9450  xleaddadd  10009  qdclt  10388  frec2uzf1od  10551  expnegap0  10692  bcval5  10908  zfz1isolemiso  10984  seq3coll  10987  fisumss  11703  fprodssdc  11901  nninfctlemfo  12361  rpdvds  12421  oddpwdclemodd  12494  pceq0  12645  pcmpt  12666  gsumfzval  13223  ply1termlem  15214  lgseisenlem1  15547  lgsquadlem3  15556  2sqlem8a  15599  2sqlem8  15600  2omap  15932  pwle2  15935