Theorem negbid 463

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 400	. 2 |- ((ps <-> ch) <-> (-. ps <-> -. ch))
3	1, 2	sylib 173	1 |- (ph -> (-. ps <-> -. ch))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127

This theorem is referenced by:  imbi1d 465  con3th 573  eqsex 834  cbvex 849  cbvexd 978  neeq1 1194  neeq2 1195  neleq1 1199  neleq2 1200  gencbval 1373  cla4egf 1395  cla42gv 1399  cla4ev 1401  ru 1437  sbcn 1459  nalset 1482  eldif 1496  difeq2 1583  prel12 1875  nnullss 1880  dtru 1889  opprc1b 1906  poeq1 2130  pocl 2132  sotric 2148  sotrieq 2149  so 2152  supmo 2156  supub 2160  suplub 2161  supsn 2168  fri 2170  dffr2 2171  frc 2172  freq1 2174  fr2nr 2177  fr3nr 2178  efrirr 2180  tz7.2 2183  wereu 2197  limeq 2211  nordeq 2218  ordtri1 2231  ordtri3 2234  ordsucsssuc 2325  orduninsuc 2365  dfom2 2374  omssnlim 2386  ssnlim 2407  vtoclibr 2451  weinxp 2467  tz6.12i 2847  fvco 2865  cbvexfo 2924  isofrlem 2939  f1oweOLD 2944  canth 2945  tfrlem10 2958  tz7.44-2 2967  rdglem2 2976  tz7.48lem 2993  tz7.49 2997  abianfp 3000  ndmoprg 3057  oacan 3150  2dom 3332  php 3409  nndomo 3416  nnsdomo 3417  omsdomnn 3424  unfilem1 3438  fiint 3445  zfregcl 3446  eirrv 3449  eirr 3450  en2lp 3453  inf3lem2 3465  rankr1g 3519  cplem2 3546  aceq3lem 3555  aceq5lem3 3560  aceq5lem4 3561  aceq5 3563  aceq6b 3565  ac6lem 3575  kmlem1 3580  kmlem2 3581  kmlem4 3583  kmlem11 3590  kmlem14 3593  numthlem 3598  zornlem6 3608  zorn 3611  fodomb 3615  hta 3619  cardsdom 3643  domtri 3644  alephord3 3683  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregnd 3750  ltsopi 3810  addnidpi 3822  ltsopq 3869  genpnnp 3902  ltexprlem7 3942  addcanpr 3946  prlem936 3949  reclem1pr 3950  reclem3pr 3952  suppr 3957  ltsosr 3997  suppsr 4016  supsrlem6 4024  supre 4054  ltsor 4055  muln0bt 4213  divneq0bt 4230  leltt 4278  ltsqt 4376  ledivt 4405  le2sq 4415  lt0nnn0 4549  indstr 4611  sqrlem18 4748  sqrlem21 4751  sqrlem22 4752  sqr2irrlem3 4779  absgt0t 4863  ruclem29 4913  ruclem35 4919  ruclem37 4921  ruclem39 4923  infxpidmlem10 4942  infxpidmlem11 4943  shintclt 5295  chintclt 5297  ch0psst 5370  chpsscon3t 5420  chnlet 5431  chne0t 5452  elspansn2t 5472  pjnelt 5667  str 5698  cvbrt 5714  cvcon3t 5716  chcv1t 5751  cvexchlem 5759  chrelat2t 5761  atnem0 5766  atcvat2 5772

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org