Theorem mtbird 645

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)

Hypotheses

Ref	Expression
mtbird.min	⊢ (𝜑 → ¬ 𝜒)
mtbird.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mtbird	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtbird

Step	Hyp	Ref	Expression
1		mtbird.min	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtbird.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 635	1 ⊢ (𝜑 → ¬ 𝜓)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-in1 586  ax-in2 587

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqneltrd  2210  neleqtrrd  2213  fidifsnen  6717  php5fin  6729  tridc  6746  fimax2gtrilemstep  6747  en2eqpr  6754  inflbti  6863  omp1eomlem  6931  difinfsnlem  6936  addnidpig  7092  nqnq0pi  7194  ltpopr  7351  cauappcvgprlemladdru  7412  caucvgprlemladdrl  7434  caucvgprprlemnkltj  7445  caucvgprprlemnkeqj  7446  caucvgprprlemaddq  7464  ltposr  7506  axltirr  7755  reapirr  8257  apirr  8285  indstr2  9305  xrltnsym  9472  xrlttr  9474  xrltso  9475  xltadd1  9552  xposdif  9558  xleaddadd  9563  lbioog  9589  ubioog  9590  fzn  9715  flqltnz  9953  iseqf1olemnab  10154  iseqf1olemqk  10160  exp3val  10188  zfz1isolemiso  10475  xrmaxltsup  10919  binomlem  11144  dvdsle  11390  2tp1odd  11429  divalglemeuneg  11468  bezoutlemle  11542  rpexp  11677  oddpwdclemxy  11692  oddpwdclemndvds  11694  sqpweven  11698  2sqpwodd  11699  ctinfom  11786