Theorem notbid 614

Description: Deduction negating both sides of a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem notbid

Step	Hyp	Ref	Expression
1		bid.1	. 2 |- (ph -> (ps <-> ch))
2		notbi 525	. 2 |- ((ps <-> ch) <-> (-. ps <-> -. ch))
3	1, 2	sylib 196	1 |- (ph -> (-. ps <-> -. ch))

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

This theorem is referenced by:  imbi1d 616  con3th 771  equsex 1189  drex1 1193  cbvex 1203  hbsb4 1286  cbvexd 1359  ax11inda 1410  2mo 1487  neeq1 1633  neeq2 1634  necon3abid 1642  neleq1 1688  neleq2 1689  gencbval 1886  cla4egf 1907  cla42gv 1911  cla43gv 1913  ru 1984  sbcng 2017  sbcrext 2041  sbcrexgf 2043  eldif 2109  difeq2 2206  disjne 2368  prel12 2549  nalset 2786  dtru 2831  dtruALT 2848  opprc1b 2872  poeq1 2920  pocl 2922  posn 2928  sotric 2939  sotrieq 2940  so 2943  dffr2 2949  freq1 2952  efrirr 2957  tz7.2 2959  wereu 2972  nordeq 2994  ordtri1 3008  ordtri3 3011  rexxfrd 3121  rexxfr 3124  elpwunsn 3135  ordsucsssuc 3179  orduninsuc 3197  dfom2 3220  omssnlim 3232  ssnlim 3236  vtoclibr 3296  rexxp 3302  rexxpf 3304  weinxp 3319  cnvpo 3627  fvco 3885  cbvexfo 4000  f1oweALT 4020  ndmoprg 4104  canth 4205  tz7.44-2 4230  rdglem2 4239  tz7.48lem 4256  abianfp 4263  oacan 4318  omlimcl 4345  nneob 4395  2dom 4568  0sdomg 4611  php 4660  nndomo 4667  nnsdomo 4668  omsdomnn 4676  unfilem1 4694  supmo 4719  supub 4723  suplub 4724  supmaxlem 4731  suppr 4733  supsnALT 4735  zfregcl 4738  elirrv 4741  elirr 4742  en2lp 4747  noinfep 4786  rankr1g 4821  hta 4874  ac6n 4903  kmlem2 4912  kmlem4 4914  zorn2 4942  domtri 4987  alephord3 5028  alephval3 5053  axpowndlem2 5104  axpowndlem3 5105  axpowndlem4 5106  axregnd 5110  ltsopi 5170  addnidpi 5182  ltsopq 5229  genpnnp 5262  ltexprlem7 5302  addcanpr 5306  prlem936 5309  reclem1pr 5310  reclem3pr 5312  supexpr 5317  ltsosr 5357  suppsr 5376  supsrlem6 5384  supre 5414  ltsor 5415  xrlenlt 5655  axlttri 5657  axsup 5661  muln0b 5849  lediv1 5995  lediv1OLD 5996  lemuldiv 6020  le2msqi 6027  rpneg 6211  lbinfm 6216  infm3 6222  infmsup 6236  xrsupexmnf 6242  xrinfmexpnf 6243  xrsupsslem 6244  xrinfmsslem 6245  xrub 6248  supxr 6249  supxrre 6251  lt0nnn0 6284  znnnlt1 6324  nneo 6369  qbtwnxr 6419  indstr 6588  sqrlem18 6891  sqrlem21 6894  sqrlem22 6895  sqr2irrlem3 6927  bccl2 7174  climrecl 7313  climge0 7315  climubii 7356  eirr 7599  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  ruclem29 7750  ruclem35 7756  ruclem37 7758  ruclem39 7760  infxpidmlem10 7773  clsval2 7895  elcls 7914  bl2in 8053  tgioolem 8125  dscmet 8129  bcthlem9 8218  bcthlem33 8242  spwnex 8923  efif1lem6 9007  chpsscon3 9702  chnle 9713  nonbooli 9874  pjnel 9949  specval 10104  nmcoplbi 10237  nmcfnlbi 10266  stri 10465  hstri 10473  cvbr 10490  cvcon3 10492  chcv1 10563  cvexchlem 10576  chrelat2 10578  atnem0OLD 10586  fiiu 10738  vxveqv 10761  fiiu2 10852  cdrci 10994  isfil 11071  fipfil2 11077  efilcp2 11087  cnfilca 11088  rcfpfillem2 11090  bwt2 11123  iintlem1 11155  lpni 11417  ordiso 11426  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  omsubss 11445  omsubdmss 11447  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  connsub 11502  reconnlem4 11510  t0dist 11602  ist1-2 11603  ist1-3 11604  t1sep 11607  fbasfip 11627  fbunfip 11631  fgfil 11638  extbas1 11641  filrn 11643  filfinnfr 11646  filssufil 11656  ufileu 11658  ufinffr 11663  flimcls 11684  hausfillim 11685  flimfcls 11725  flimfnfcls 11727  filnet 11768  inficl 11849  supubt 11855  fsumlt1 11894  heiborlem20 12030

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 145  df-an 223

Copyright terms: Public domain