Theorem mtbid 678

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  682  eqneltrrd  2328  neleqtrd  2329  eueq3dc  2980  efrirr  4450  fidcenumlemrks  7152  nqnq0pi  7658  zdclt  9557  xleaddadd  10122  qdclt  10506  frec2uzf1od  10669  expnegap0  10810  bcval5  11026  zfz1isolemiso  11104  seq3coll  11107  fisumss  11971  fprodssdc  12169  nninfctlemfo  12629  rpdvds  12689  oddpwdclemodd  12762  pceq0  12913  pcmpt  12934  gsumfzval  13492  ply1termlem  15485  lgseisenlem1  15818  lgsquadlem3  15827  2sqlem8a  15870  2sqlem8  15871  2omap  16645  pwle2  16650