Theorem negbid 610

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 521	. 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 612  con3th 765  equsex 1150  drex1 1154  cbvex 1164  hbsb4 1246  cbvexd 1319  ax11inda 1369  2mo 1445  neeq1 1587  neeq2 1588  necon3abid 1596  neleq1 1639  neleq2 1640  gencbval 1836  cla4egf 1857  cla42gv 1861  cla43gv 1863  ru 1934  sbcng 1965  sbcrext 1987  sbcrexgf 1989  eldif 2053  difeq2 2150  disjne 2311  prel12 2480  nalset 2707  dtruALT 2743  dtru 2767  opprc1b 2791  poeq1 2837  pocl 2839  sotric 2855  sotrieq 2856  so 2859  rexxfrd 2893  rexxfr 2896  elpwunsn 2907  dffr2 2914  freq1 2917  efrirr 2923  tz7.2 2926  wereu 2940  nordeq 2962  ordtri1 2975  ordtri3 2978  ordsucsssuc 3069  orduninsuc 3109  dfom2 3128  omssnlim 3140  ssnlim 3162  vtoclibr 3208  rexxp 3214  weinxp 3228  cnvpo 3514  fvco 3765  cbvexfo 3877  f1oweALT 3897  canth 3898  tz7.44-2 3920  rdglem2 3929  tz7.48lem 3946  abianfp 3953  ndmoprg 4034  ndmoprgOLD 4035  oacan 4172  omlimcl 4199  nneob 4245  2dom 4414  0sdomg 4452  php 4499  nndomo 4506  nnsdomo 4507  omsdomnn 4515  unfilem1 4530  supmo 4556  supub 4560  suplub 4561  supmaxlem 4568  suppr 4570  supsnALT 4572  zfregcl 4575  elirrv 4578  elirr 4579  en2lp 4582  noinfep 4620  rankr1g 4655  hta 4708  ac6n 4737  kmlem2 4746  kmlem4 4748  zorn2 4776  domtri 4818  alephord3 4858  alephval3 4883  axpowndlem2 4930  axpowndlem3 4931  axpowndlem4 4932  axregnd 4936  ltsopi 4996  addnidpi 5008  ltsopq 5055  genpnnp 5088  ltexprlem7 5128  addcanpr 5132  prlem936 5135  reclem1pr 5136  reclem3pr 5138  supexpr 5143  ltsosr 5183  suppsr 5202  supsrlem6 5210  supre 5240  ltsor 5241  xrlenltt 5481  axlttri 5483  axsup 5487  muln0bt 5674  lediv1t 5814  lemuldivt 5832  le2msq 5838  lbinfm 6003  infm3 6009  infmsup 6023  xrsupexmnf 6029  xrinfmexpnf 6030  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxr 6036  supxrre 6038  lt0nnn0 6071  znnnlt1t 6111  nneot 6153  qbtwnxr 6225  indstr 6401  sqrlem18 6628  sqrlem21 6631  sqrlem22 6632  sqr2irrlem3 6664  bccl2t 6917  climrecl 7055  climge0 7057  climubi 7097  eirr 7343  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  ruclem29 7489  ruclem35 7495  ruclem37 7497  ruclem39 7499  infxpidmlem10 7512  clsval2 7635  elcls 7654  bl2in 7795  tgioolem 7866  dscmet 7870  bcthlem9 7957  bcthlem33 7981  spwnex 8602  efif1lem6 8669  chpsscon3t 9364  chnlet 9375  nonbool 9536  pjnelt 9611  eigortht 9704  specvalt 9764  eighmortht 9827  nmcoplb 9896  nmcfnlb 9925  str 10122  hstr 10130  cvbrt 10147  cvcon3t 10149  chcv1t 10219  cvexchlem 10232  chrelat2t 10234  atnem0 10241  gelcomplOLD 10353  gelsupvalOLD 10354  fiiu 10386  fiiu2 10413  cdrci 10417  isfil 10469  fipfil2 10475  efilcp2 10486  cnfilca 10487  iintlem1 10512

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