Theorem mtbird 679

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 669	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2327  neleqtrrd  2330  eqnbrtrd  4106  fidifsnen  7057  php5fin  7071  tridc  7089  fimax2gtrilemstep  7090  en2eqpr  7099  inflbti  7223  omp1eomlem  7293  difinfsnlem  7298  addnidpig  7556  nqnq0pi  7658  ltpopr  7815  cauappcvgprlemladdru  7876  caucvgprlemladdrl  7898  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemaddq  7928  ltposr  7983  axpre-suploclemres  8121  axltirr  8246  reapirr  8757  apirr  8785  indstr2  9843  xrltnsym  10028  xrlttr  10030  xrltso  10031  xltadd1  10111  xposdif  10117  xleaddadd  10122  lbioog  10148  ubioog  10149  fzn  10277  xqltnle  10528  flqltnz  10548  iseqf1olemnab  10764  iseqf1olemqk  10770  exp3val  10804  fihashelne0d  11060  zfz1isolemiso  11104  swrdnd  11241  swrd0g  11242  xrmaxltsup  11820  binomlem  12046  dvdsle  12407  2tp1odd  12447  divalglemeuneg  12486  bits0e  12512  bezoutlemle  12581  rpexp  12727  oddpwdclemxy  12743  oddpwdclemndvds  12745  sqpweven  12749  2sqpwodd  12750  oddprm  12834  pythagtriplem11  12849  pythagtriplem13  12851  pcpremul  12868  pczndvds2  12893  pc2dvds  12905  pcmpt  12918  ctinfom  13051  aprirr  14300  ivthinc  15370  logbgcd1irraplemexp  15695  lgsval2lem  15742  lgsdir  15767  lgsne0  15770  gausslemma2dlem1f1o  15792  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem4  15805  lgsquadlem1  15809  lgsquad2  15815  m1lgs  15817  2sqlem7  15853  1loopgrvd0fi  16160  neapmkvlem  16692