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 763  equsex 1135  drex1 1139  cbvex 1149  hbsb4 1232  cbvexd 1303  ax11inda 1348  2mo 1424  neeq1 1566  neeq2 1567  necon3abid 1575  neleq1 1618  neleq2 1619  gencbval 1815  cla4egf 1836  cla42gv 1840  ru 1909  sbcng 1940  sbcrext 1962  sbcrexgf 1964  eldif 2028  difeq2 2125  disjne 2286  prel12 2454  nalset 2680  dtruALT 2716  dtru 2740  opprc1b 2763  poeq1 2806  pocl 2808  sotric 2824  sotrieq 2825  so 2828  rexxfrd 2861  rexxfr 2864  elpwunsn 2875  dffr2 2882  freq1 2885  efrirr 2891  tz7.2 2894  wereu 2908  nordeq 2930  ordtri1 2943  ordtri3 2946  ordsucsssuc 3037  orduninsuc 3077  dfom2 3096  omssnlim 3108  ssnlim 3130  vtoclibr 3175  rexxp 3181  weinxp 3195  cnvpo 3463  fvco 3713  cbvexfo 3825  f1oweALT 3845  canth 3846  tz7.44-2 3868  rdglem2 3877  tz7.48lem 3894  abianfp 3901  ndmoprg 3982  ndmoprgOLD 3983  oacan 4120  omlimcl 4147  nneob 4193  2dom 4362  0sdomg 4400  php 4445  nndomo 4452  nnsdomo 4453  omsdomnn 4461  unfilem1 4476  supmo 4502  supub 4506  suplub 4507  suppr 4514  supsnALT 4516  zfregcl 4519  elirrv 4522  elirr 4523  en2lp 4526  noinfep 4564  rankr1g 4599  hta 4652  ac6n 4681  kmlem2 4690  kmlem4 4692  zorn2 4720  domtri 4761  alephord3 4801  alephval3 4826  axpowndlem2 4873  axpowndlem3 4874  axpowndlem4 4875  axregnd 4879  ltsopi 4939  addnidpi 4951  ltsopq 4998  genpnnp 5031  ltexprlem7 5071  addcanpr 5075  prlem936 5078  reclem1pr 5079  reclem3pr 5081  supexpr 5086  ltsosr 5126  suppsr 5145  supsrlem6 5153  supre 5183  ltsor 5184  xrlenltt 5424  axlttri 5426  axsup 5430  muln0bt 5617  lediv1t 5757  lemuldivt 5775  le2msq 5781  lbinfm 5946  infm3 5952  infmsup 5966  xrsupexmnf 5972  xrinfmexpnf 5973  xrsupsslem 5974  xrinfmsslem 5975  xrub 5978  supxr 5979  supxrre 5981  lt0nnn0 6014  znnnlt1t 6054  nneot 6096  qbtwnxr 6168  indstr 6344  sqrlem18 6571  sqrlem21 6574  sqrlem22 6575  sqr2irrlem3 6607  bccl2t 6860  climrecl 6998  climge0 7000  climubi 7040  eirr 7286  acdc3 7380  acdc2 7383  acdc5 7386  acdc 7388  ruclem29 7432  ruclem35 7438  ruclem37 7440  ruclem39 7442  infxpidmlem10 7455  clsval2 7578  elcls 7596  bl2in 7731  tgioolem 7801  dscmet 7804  bcthlem9 7889  bcthlem33 7913  efif1lem6 8563  fiiu 8709  fiiu2 8734  cdrci 8738  isfil 8783  fipfil2 8789  efilcp2 8800  cnfilca 8801  iintlem1 8826  chpsscon3t 9555  chnlet 9566  nonbool 9727  pjnelt 9802  eigortht 9895  specvalt 9955  eighmortht 10018  nmcoplb 10087  nmcfnlb 10116  str 10308  hstr 10316  cvbrt 10333  cvcon3t 10335  chcv1t 10404  cvexchlem 10417  chrelat2t 10419  atnem0 10426

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