Theorem mtbird 675

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 665	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  2302  neleqtrrd  2305  eqnbrtrd  4065  fidifsnen  6974  php5fin  6986  tridc  7003  fimax2gtrilemstep  7004  en2eqpr  7011  inflbti  7133  omp1eomlem  7203  difinfsnlem  7208  addnidpig  7456  nqnq0pi  7558  ltpopr  7715  cauappcvgprlemladdru  7776  caucvgprlemladdrl  7798  caucvgprprlemnkltj  7809  caucvgprprlemnkeqj  7810  caucvgprprlemaddq  7828  ltposr  7883  axpre-suploclemres  8021  axltirr  8146  reapirr  8657  apirr  8685  indstr2  9737  xrltnsym  9922  xrlttr  9924  xrltso  9925  xltadd1  10005  xposdif  10011  xleaddadd  10016  lbioog  10042  ubioog  10043  fzn  10171  xqltnle  10417  flqltnz  10437  iseqf1olemnab  10653  iseqf1olemqk  10659  exp3val  10693  fihashelne0d  10949  zfz1isolemiso  10991  swrdnd  11120  swrd0g  11121  xrmaxltsup  11613  binomlem  11838  dvdsle  12199  2tp1odd  12239  divalglemeuneg  12278  bits0e  12304  bezoutlemle  12373  rpexp  12519  oddpwdclemxy  12535  oddpwdclemndvds  12537  sqpweven  12541  2sqpwodd  12542  oddprm  12626  pythagtriplem11  12641  pythagtriplem13  12643  pcpremul  12660  pczndvds2  12685  pc2dvds  12697  pcmpt  12710  ctinfom  12843  aprirr  14089  ivthinc  15159  logbgcd1irraplemexp  15484  lgsval2lem  15531  lgsdir  15556  lgsne0  15559  gausslemma2dlem1f1o  15581  lgseisenlem1  15591  lgseisenlem2  15592  lgseisenlem4  15594  lgsquadlem1  15598  lgsquad2  15604  m1lgs  15606  2sqlem7  15642  neapmkvlem  16080