Theorem negbid 609

Description: Deduction negating both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
negbid	|- (ph -> (-. ps <-> -. ch))

Proof of Theorem negbid

Step	Hyp	Ref	Expression
1		bid.1	. 2 |- (ph -> (ps <-> ch))
2		pm4.11 520	. 2 |- ((ps <-> ch) <-> (-. ps <-> -. ch))
3	1, 2	sylib 198	1 |- (ph -> (-. ps <-> -. ch))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  imbi1d 611  con3th 764  equsex 1148  drex1 1152  cbvex 1162  hbsb4 1243  cbvexd 1316  ax11inda 1364  2mo 1440  neeq1 1582  neeq2 1583  necon3abid 1591  neleq1 1634  neleq2 1635  gencbval 1831  cla4egf 1852  cla42gv 1856  cla43gv 1858  ru 1928  sbcng 1959  sbcrext 1981  sbcrexgf 1983  eldif 2047  difeq2 2144  disjne 2305  prel12 2475  nalset 2702  dtruALT 2738  dtru 2762  opprc1b 2786  poeq1 2833  pocl 2835  sotric 2851  sotrieq 2852  so 2855  rexxfrd 2888  rexxfr 2891  elpwunsn 2902  dffr2 2909  freq1 2912  efrirr 2918  tz7.2 2921  wereu 2935  nordeq 2957  ordtri1 2970  ordtri3 2973  ordsucsssuc 3064  orduninsuc 3104  dfom2 3123  omssnlim 3135  ssnlim 3157  vtoclibr 3203  rexxp 3209  weinxp 3223  cnvpo 3508  fvco 3759  cbvexfo 3871  f1oweALT 3891  canth 3892  tz7.44-2 3914  rdglem2 3923  tz7.48lem 3940  abianfp 3947  ndmoprg 4028  ndmoprgOLD 4029  oacan 4166  omlimcl 4193  nneob 4239  2dom 4408  0sdomg 4446  php 4493  nndomo 4500  nnsdomo 4501  omsdomnn 4509  unfilem1 4524  supmo 4550  supub 4554  suplub 4555  suppr 4562  supsnALT 4564  zfregcl 4567  elirrv 4570  elirr 4571  en2lp 4574  noinfep 4612  rankr1g 4647  hta 4700  ac6n 4729  kmlem2 4738  kmlem4 4740  zorn2 4768  domtri 4810  alephord3 4850  alephval3 4875  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregnd 4928  ltsopi 4988  addnidpi 5000  ltsopq 5047  genpnnp 5080  ltexprlem7 5120  addcanpr 5124  prlem936 5127  reclem1pr 5128  reclem3pr 5130  supexpr 5135  ltsosr 5175  suppsr 5194  supsrlem6 5202  supre 5232  ltsor 5233  xrlenltt 5473  axlttri 5475  axsup 5479  muln0bt 5666  lediv1t 5806  lemuldivt 5824  le2msq 5830  lbinfm 5995  infm3 6001  infmsup 6015  xrsupexmnf 6021  xrinfmexpnf 6022  xrsupsslem 6023  xrinfmsslem 6024  xrub 6027  supxr 6028  supxrre 6030  lt0nnn0 6063  znnnlt1t 6103  nneot 6145  qbtwnxr 6217  indstr 6393  sqrlem18 6620  sqrlem21 6623  sqrlem22 6624  sqr2irrlem3 6656  bccl2t 6909  climrecl 7047  climge0 7049  climubi 7089  eirr 7335  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  ruclem29 7481  ruclem35 7487  ruclem37 7489  ruclem39 7491  infxpidmlem10 7504  clsval2 7627  elcls 7646  bl2in 7783  tgioolem 7853  dscmet 7856  bcthlem9 7941  bcthlem33 7965  efif1lem6 8650  chpsscon3t 9341  chnlet 9352  nonbool 9513  pjnelt 9588  eigortht 9681  specvalt 9741  eighmortht 9804  nmcoplb 9873  nmcfnlb 9902  str 10094  hstr 10102  cvbrt 10119  cvcon3t 10121  chcv1t 10190  cvexchlem 10203  chrelat2t 10205  atnem0 10212  fiiu 10350  fiiu2 10377  cdrci 10381  isfil 10433  fipfil2 10439  efilcp2 10450  cnfilca 10451  iintlem1 10476

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain