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  7023  nqnq0pi  7510  zdclt  9408  xleaddadd  9967  qdclt  10340  frec2uzf1od  10503  expnegap0  10644  bcval5  10860  zfz1isolemiso  10936  seq3coll  10939  fisumss  11562  fprodssdc  11760  nninfctlemfo  12220  rpdvds  12280  oddpwdclemodd  12353  pceq0  12504  pcmpt  12525  gsumfzval  13081  ply1termlem  15025  lgseisenlem1  15358  lgsquadlem3  15367  2sqlem8a  15410  2sqlem8  15411  2omap  15689  pwle2  15692