Theorem mtbid 662

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 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	mtod 653	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnib  666  eqneltrrd  2262  neleqtrd  2263  eueq3dc  2899  efrirr  4330  fidcenumlemrks  6914  nqnq0pi  7375  zdclt  9264  xleaddadd  9819  frec2uzf1od  10337  expnegap0  10459  bcval5  10672  zfz1isolemiso  10748  seq3coll  10751  fisumss  11329  fprodssdc  11527  rpdvds  12027  oddpwdclemodd  12100  pceq0  12249  pcmpt  12269  2sqlem8a  13558  2sqlem8  13559  pwle2  13838