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  2325  neleqtrrd  2328  eqnbrtrd  4101  fidifsnen  7045  php5fin  7057  tridc  7075  fimax2gtrilemstep  7076  en2eqpr  7085  inflbti  7207  omp1eomlem  7277  difinfsnlem  7282  addnidpig  7539  nqnq0pi  7641  ltpopr  7798  cauappcvgprlemladdru  7859  caucvgprlemladdrl  7881  caucvgprprlemnkltj  7892  caucvgprprlemnkeqj  7893  caucvgprprlemaddq  7911  ltposr  7966  axpre-suploclemres  8104  axltirr  8229  reapirr  8740  apirr  8768  indstr2  9821  xrltnsym  10006  xrlttr  10008  xrltso  10009  xltadd1  10089  xposdif  10095  xleaddadd  10100  lbioog  10126  ubioog  10127  fzn  10255  xqltnle  10504  flqltnz  10524  iseqf1olemnab  10740  iseqf1olemqk  10746  exp3val  10780  fihashelne0d  11036  zfz1isolemiso  11079  swrdnd  11212  swrd0g  11213  xrmaxltsup  11790  binomlem  12015  dvdsle  12376  2tp1odd  12416  divalglemeuneg  12455  bits0e  12481  bezoutlemle  12550  rpexp  12696  oddpwdclemxy  12712  oddpwdclemndvds  12714  sqpweven  12718  2sqpwodd  12719  oddprm  12803  pythagtriplem11  12818  pythagtriplem13  12820  pcpremul  12837  pczndvds2  12862  pc2dvds  12874  pcmpt  12887  ctinfom  13020  aprirr  14268  ivthinc  15338  logbgcd1irraplemexp  15663  lgsval2lem  15710  lgsdir  15735  lgsne0  15738  gausslemma2dlem1f1o  15760  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem4  15773  lgsquadlem1  15777  lgsquad2  15783  m1lgs  15785  2sqlem7  15821  neapmkvlem  16549