Theorem mtbird 677

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 667	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2305  neleqtrrd  2308  eqnbrtrd  4080  fidifsnen  7000  php5fin  7012  tridc  7029  fimax2gtrilemstep  7030  en2eqpr  7037  inflbti  7159  omp1eomlem  7229  difinfsnlem  7234  addnidpig  7491  nqnq0pi  7593  ltpopr  7750  cauappcvgprlemladdru  7811  caucvgprlemladdrl  7833  caucvgprprlemnkltj  7844  caucvgprprlemnkeqj  7845  caucvgprprlemaddq  7863  ltposr  7918  axpre-suploclemres  8056  axltirr  8181  reapirr  8692  apirr  8720  indstr2  9772  xrltnsym  9957  xrlttr  9959  xrltso  9960  xltadd1  10040  xposdif  10046  xleaddadd  10051  lbioog  10077  ubioog  10078  fzn  10206  xqltnle  10454  flqltnz  10474  iseqf1olemnab  10690  iseqf1olemqk  10696  exp3val  10730  fihashelne0d  10986  zfz1isolemiso  11028  swrdnd  11157  swrd0g  11158  xrmaxltsup  11735  binomlem  11960  dvdsle  12321  2tp1odd  12361  divalglemeuneg  12400  bits0e  12426  bezoutlemle  12495  rpexp  12641  oddpwdclemxy  12657  oddpwdclemndvds  12659  sqpweven  12663  2sqpwodd  12664  oddprm  12748  pythagtriplem11  12763  pythagtriplem13  12765  pcpremul  12782  pczndvds2  12807  pc2dvds  12819  pcmpt  12832  ctinfom  12965  aprirr  14212  ivthinc  15282  logbgcd1irraplemexp  15607  lgsval2lem  15654  lgsdir  15679  lgsne0  15682  gausslemma2dlem1f1o  15704  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem4  15717  lgsquadlem1  15721  lgsquad2  15727  m1lgs  15729  2sqlem7  15765  neapmkvlem  16346