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  7422  nqnq0pi  7524  ltpopr  7681  cauappcvgprlemladdru  7742  caucvgprlemladdrl  7764  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemaddq  7794  ltposr  7849  axpre-suploclemres  7987  axltirr  8112  reapirr  8623  apirr  8651  indstr2  9702  xrltnsym  9887  xrlttr  9889  xrltso  9890  xltadd1  9970  xposdif  9976  xleaddadd  9981  lbioog  10007  ubioog  10008  fzn  10136  xqltnle  10376  flqltnz  10396  iseqf1olemnab  10612  iseqf1olemqk  10618  exp3val  10652  fihashelne0d  10908  zfz1isolemiso  10950  xrmaxltsup  11442  binomlem  11667  dvdsle  12028  2tp1odd  12068  divalglemeuneg  12107  bits0e  12133  bezoutlemle  12202  rpexp  12348  oddpwdclemxy  12364  oddpwdclemndvds  12366  sqpweven  12370  2sqpwodd  12371  oddprm  12455  pythagtriplem11  12470  pythagtriplem13  12472  pcpremul  12489  pczndvds2  12514  pc2dvds  12526  pcmpt  12539  ctinfom  12672  aprirr  13917  ivthinc  14965  logbgcd1irraplemexp  15290  lgsval2lem  15337  lgsdir  15362  lgsne0  15365  gausslemma2dlem1f1o  15387  lgseisenlem1  15397  lgseisenlem2  15398  lgseisenlem4  15400  lgsquadlem1  15404  lgsquad2  15410  m1lgs  15412  2sqlem7  15448  neapmkvlem  15802