Theorem mtbid 676

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 667	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  680  eqneltrrd  2326  neleqtrd  2327  eueq3dc  2977  efrirr  4444  fidcenumlemrks  7131  nqnq0pi  7636  zdclt  9535  xleaddadd  10095  qdclt  10477  frec2uzf1od  10640  expnegap0  10781  bcval5  10997  zfz1isolemiso  11074  seq3coll  11077  fisumss  11919  fprodssdc  12117  nninfctlemfo  12577  rpdvds  12637  oddpwdclemodd  12710  pceq0  12861  pcmpt  12882  gsumfzval  13440  ply1termlem  15432  lgseisenlem1  15765  lgsquadlem3  15774  2sqlem8a  15817  2sqlem8  15818  2omap  16446  pwle2  16451