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  2292  neleqtrrd  2295  eqnbrtrd  4052  fidifsnen  6940  php5fin  6952  tridc  6969  fimax2gtrilemstep  6970  en2eqpr  6977  inflbti  7099  omp1eomlem  7169  difinfsnlem  7174  addnidpig  7420  nqnq0pi  7522  ltpopr  7679  cauappcvgprlemladdru  7740  caucvgprlemladdrl  7762  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemaddq  7792  ltposr  7847  axpre-suploclemres  7985  axltirr  8110  reapirr  8621  apirr  8649  indstr2  9700  xrltnsym  9885  xrlttr  9887  xrltso  9888  xltadd1  9968  xposdif  9974  xleaddadd  9979  lbioog  10005  ubioog  10006  fzn  10134  xqltnle  10374  flqltnz  10394  iseqf1olemnab  10610  iseqf1olemqk  10616  exp3val  10650  fihashelne0d  10906  zfz1isolemiso  10948  xrmaxltsup  11440  binomlem  11665  dvdsle  12026  2tp1odd  12066  divalglemeuneg  12105  bits0e  12131  bezoutlemle  12200  rpexp  12346  oddpwdclemxy  12362  oddpwdclemndvds  12364  sqpweven  12368  2sqpwodd  12369  oddprm  12453  pythagtriplem11  12468  pythagtriplem13  12470  pcpremul  12487  pczndvds2  12512  pc2dvds  12524  pcmpt  12537  ctinfom  12670  aprirr  13915  ivthinc  14963  logbgcd1irraplemexp  15288  lgsval2lem  15335  lgsdir  15360  lgsne0  15363  gausslemma2dlem1f1o  15385  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem4  15398  lgsquadlem1  15402  lgsquad2  15408  m1lgs  15410  2sqlem7  15446  neapmkvlem  15798