Theorem mtbird 663

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 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-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqneltrd  2253  neleqtrrd  2256  fidifsnen  6808  php5fin  6820  tridc  6837  fimax2gtrilemstep  6838  en2eqpr  6845  inflbti  6960  omp1eomlem  7028  difinfsnlem  7033  addnidpig  7239  nqnq0pi  7341  ltpopr  7498  cauappcvgprlemladdru  7559  caucvgprlemladdrl  7581  caucvgprprlemnkltj  7592  caucvgprprlemnkeqj  7593  caucvgprprlemaddq  7611  ltposr  7666  axpre-suploclemres  7804  axltirr  7927  reapirr  8435  apirr  8463  indstr2  9502  xrltnsym  9682  xrlttr  9684  xrltso  9685  xltadd1  9762  xposdif  9768  xleaddadd  9773  lbioog  9799  ubioog  9800  fzn  9926  flqltnz  10168  iseqf1olemnab  10369  iseqf1olemqk  10375  exp3val  10403  zfz1isolemiso  10692  xrmaxltsup  11137  binomlem  11362  dvdsle  11717  2tp1odd  11756  divalglemeuneg  11795  bezoutlemle  11872  rpexp  12007  oddpwdclemxy  12023  oddpwdclemndvds  12025  sqpweven  12029  2sqpwodd  12030  ctinfom  12129  ivthinc  12981  logbgcd1irraplemexp  13245  neapmkvlem  13600