Theorem mtbid 673

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 664	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  677  eqneltrrd  2293  neleqtrd  2294  eueq3dc  2938  efrirr  4389  fidcenumlemrks  7028  nqnq0pi  7522  zdclt  9420  xleaddadd  9979  qdclt  10352  frec2uzf1od  10515  expnegap0  10656  bcval5  10872  zfz1isolemiso  10948  seq3coll  10951  fisumss  11574  fprodssdc  11772  nninfctlemfo  12232  rpdvds  12292  oddpwdclemodd  12365  pceq0  12516  pcmpt  12537  gsumfzval  13093  ply1termlem  15062  lgseisenlem1  15395  lgsquadlem3  15404  2sqlem8a  15447  2sqlem8  15448  2omap  15726  pwle2  15729