Theorem mtbird 684

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 673	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  eqneltrd  2334  neleqtrrd  2337  eqnbrtrd  4149  fidifsnen  7177  php5fin  7191  tridc  7209  fimax2gtrilemstep  7210  en2eqpr  7219  inflbti  7371  omp1eomlem  7441  difinfsnlem  7446  addnidpig  7710  nqnq0pi  7812  ltpopr  7969  cauappcvgprlemladdru  8030  caucvgprlemladdrl  8052  caucvgprprlemnkltj  8063  caucvgprprlemnkeqj  8064  caucvgprprlemaddq  8082  ltposr  8137  axpre-suploclemres  8275  axltirr  8399  reapirr  8914  apirr  8942  indstr2  10026  xrltnsym  10213  xrlttr  10215  xrltso  10216  xltadd1  10296  xposdif  10302  xleaddadd  10307  lbioog  10333  ubioog  10334  fzn  10464  xqltnle  10720  flqltnz  10744  iseqf1olemnab  10960  iseqf1olemqk  10966  exp3val  11000  fihashelne0d  11259  hashf1lem1  11308  zfz1isolemiso  11314  swrdnd  11454  swrd0g  11455  xrmaxltsup  12050  binomlem  12276  dvdsle  12637  2tp1odd  12677  divalglemeuneg  12716  bits0e  12742  bezoutlemle  12811  rpexp  12958  nnmaxpwlemxy  12974  sqpweven  12981  2sqpwodd  12982  oddprm  13068  pythagtriplem11  13083  pythagtriplem13  13085  pcpremul  13102  pczndvds2  13127  pc2dvds  13139  pcmpt  13152  ballotfilem4  13300  ctinfom  13378  aprirr  14705  ivthinc  15881  logbgcd1irraplemexp  16216  birthdaylem3  16239  chtqub  16308  lgsval2lem  16346  lgsdir  16371  lgsne0  16374  gausslemma2dlem1f1o  16396  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem4  16409  lgsquadlem1  16413  lgsquad2  16419  m1lgs  16421  2sqlem7  16457  1loopgrvd0fi  16764  rirrdisj  17303  qdiff  17317  neapmkvlem  17336