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  2912  efrirr  4354  fidcenumlemrks  6952  nqnq0pi  7437  zdclt  9330  xleaddadd  9887  frec2uzf1od  10406  expnegap0  10528  bcval5  10743  zfz1isolemiso  10819  seq3coll  10822  fisumss  11400  fprodssdc  11598  rpdvds  12099  oddpwdclemodd  12172  pceq0  12321  pcmpt  12341  lgseisenlem1  14453  2sqlem8a  14472  2sqlem8  14473  pwle2  14751