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  2290  neleqtrd  2291  eueq3dc  2934  efrirr  4384  fidcenumlemrks  7012  nqnq0pi  7498  zdclt  9394  xleaddadd  9953  qdclt  10315  frec2uzf1od  10477  expnegap0  10618  bcval5  10834  zfz1isolemiso  10910  seq3coll  10913  fisumss  11535  fprodssdc  11733  nninfctlemfo  12177  rpdvds  12237  oddpwdclemodd  12310  pceq0  12460  pcmpt  12481  gsumfzval  12974  ply1termlem  14888  lgseisenlem1  15186  2sqlem8a  15209  2sqlem8  15210  pwle2  15489