Theorem mtbird 674

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 144	. 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-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2289  neleqtrrd  2292  eqnbrtrd  4047  fidifsnen  6926  php5fin  6938  tridc  6955  fimax2gtrilemstep  6956  en2eqpr  6963  inflbti  7083  omp1eomlem  7153  difinfsnlem  7158  addnidpig  7396  nqnq0pi  7498  ltpopr  7655  cauappcvgprlemladdru  7716  caucvgprlemladdrl  7738  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemaddq  7768  ltposr  7823  axpre-suploclemres  7961  axltirr  8086  reapirr  8596  apirr  8624  indstr2  9674  xrltnsym  9859  xrlttr  9861  xrltso  9862  xltadd1  9942  xposdif  9948  xleaddadd  9953  lbioog  9979  ubioog  9980  fzn  10108  xqltnle  10336  flqltnz  10356  iseqf1olemnab  10572  iseqf1olemqk  10578  exp3val  10612  fihashelne0d  10868  zfz1isolemiso  10910  xrmaxltsup  11401  binomlem  11626  dvdsle  11986  2tp1odd  12025  divalglemeuneg  12064  bezoutlemle  12145  rpexp  12291  oddpwdclemxy  12307  oddpwdclemndvds  12309  sqpweven  12313  2sqpwodd  12314  oddprm  12397  pythagtriplem11  12412  pythagtriplem13  12414  pcpremul  12431  pczndvds2  12456  pc2dvds  12468  pcmpt  12481  ctinfom  12585  aprirr  13779  ivthinc  14797  logbgcd1irraplemexp  15100  lgsval2lem  15126  lgsdir  15151  lgsne0  15154  gausslemma2dlem1f1o  15176  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2sqlem7  15208  neapmkvlem  15557