Theorem mtbid 672

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 663	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnib  676  eqneltrrd  2274  neleqtrd  2275  eueq3dc  2911  efrirr  4351  fidcenumlemrks  6947  nqnq0pi  7432  zdclt  9324  xleaddadd  9881  frec2uzf1od  10399  expnegap0  10521  bcval5  10734  zfz1isolemiso  10810  seq3coll  10813  fisumss  11391  fprodssdc  11589  rpdvds  12089  oddpwdclemodd  12162  pceq0  12311  pcmpt  12331  2sqlem8a  14240  2sqlem8  14241  pwle2  14519