Theorem notbid 746

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

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

This theorem is referenced by:  imbi1d 748  pm5.18 983  con3th 1086  equsex 1793  drex1 1797  cbvex 1809  hbsb4 1895  cbvexd 1971  ax11inda 2026  eujustALT 2040  2mo 2110  neeq1 2273  neeq2 2274  necon3abid 2298  neleq1 2351  neleq2 2352  gencbval 2581  cla4egf 2603  cla42gv 2607  cla43gv 2609  ru 2697  sbcng 2732  sbcrext 2760  sbcrexgf 2762  difjust 2829  eldif 2840  dfpss3 2920  difeq2 2940  disjne 3123  prel12 3342  nalset 3615  dtru 3662  dtruALT 3680  opprc1b 3705  poeq1 3754  pocl 3756  posn 3762  sotric 3774  sotrieq 3775  so 3778  dffr2 3784  freq1 3787  frminex 3792  efrirr 3793  tz7.2 3795  wereu 3808  nordeq 3830  ordtri1 3844  ordtri3 3847  rexxfrd 3984  rexxfr 3987  elpwunsn 4002  dfwe2 4007  ordsucsssuc 4046  nlimsucg 4063  orduninsuc 4064  dfom2 4087  ssnlim 4104  vtoclibr 4169  rexxp 4175  rexxpf 4177  weinxp 4192  intirr 4425  cnvpo 4531  fvco 4822  cbvexfo 4957  f1oweALT 4980  ndmoprg 5069  frxp 5210  poxp 5212  canth 5249  smoword 5277  tz7.44-2 5301  rdglem2 5310  tz7.48lem 5328  abianfp 5338  oacan 5393  oaword 5394  omlimcl 5420  omeulem1 5424  nneob 5473  2dom 5647  0sdomg 5695  riotabidva 5748  php 5799  nndomo 5807  nnsdomo 5808  unxpdomlem2 5818  omsdomnn 5826  frfi 5851  unfilem1 5860  supmo 5895  supub 5899  suplub 5900  supmaxlem 5909  suppr 5911  supsnALT 5913  ordiso 5914  ordtypelem5 5919  ordtypelem6 5920  ordtypelem7 5921  ordtype 5922  zfregcl 5930  elirrv 5933  elirr 5934  en2lp 5939  noinfep 5983  rankr1g 6022  hta 6097  alephord3 6163  omsubss 6175  omsubdmss 6177  fodomnum 6209  alephval3 6233  ac6n 6327  kmlem2 6338  kmlem4 6340  zorn2 6369  domtri 6403  axpowndlem2 6468  axpowndlem3 6469  axpowndlem4 6470  axregnd 6474  ltsopi 6534  addnidpi 6546  ltsopq 6593  genpnnp 6626  ltexprlem7 6666  addcanpr 6670  prlem936 6673  reclem1pr 6674  reclem3pr 6676  supexpr 6681  ltsosr 6721  suppsr 6740  supsrlem6 6748  supre 6778  ltsor 6779  xrlenlt 6860  axlttri 6862  axsup 6866  lediv1 7366  lediv1OLD 7367  lemuldiv 7391  le2msqi 7398  rpneg 7592  lbinfm 7597  infm3 7603  infmsup 7617  xrsupexmnf 7623  xrinfmexpnf 7624  xrsupsslem 7625  xrinfmsslem 7626  xrub 7629  supxr 7630  supxrre 7632  lt0nnn0 7666  znnnlt1 7706  nneo 7753  qbtwnxr 7806  difreicc 7932  indstr 7977  fz1eqblem 8060  sqrlem18 8324  sqrlem21 8327  sqrlem22 8328  sqr2irrlem3 8360  bccl2 8608  climrecl 8766  climge0 8768  climubii 8809  eirr 9054  acdc3 9153  acdc2 9157  acdc5 9160  acdc 9162  ruclem29 9201  ruclem35 9207  ruclem37 9209  ruclem39 9211  infxpidmlem10OLD 9224  divalglem7 9296  ndvdsadd 9305  gcdn0gt0 9322  gcdneg 9326  algcvgblem 9340  isprm3 9370  1arithlem11 9404  plttr 9565  clsval2 9825  elcls 9844  bl2in 9986  tgioolem 10058  dscmet 10062  bcthlem9 10151  bcthlem33 10175  spwnex 10875  efif1lem6 10960  fiiu2 11055  isfil 11104  fipfil2 11110  fbunfip 11120  fgfil 11128  extbas1 11129  filrn 11131  hausfillim 11141  lpni 11185  chpsscon3 11893  chnle 11904  nonbooli 12063  pjnel 12138  specval 12293  nmcoplbi 12427  nmcfnlbi 12456  stri 12660  hstri 12668  cvbr 12685  cvcon3 12687  chcv1 12758  cvexchlem 12771  chrelat2 12773  bnj1185 13738  bnj1479 13926  bnj1524 13948  bnj1228 14227  bnj1390 14284  bnj1417 14301  bnj1482 14322  untelirr 14427  untsucf 14429  untangtr 14433  frirrc 14459  dfpo2 14465  dfon2lem3 14485  dfon2lem4 14486  dfon2lem7 14489  dfon2lem9 14491  distel 14511  predpoirr 14551  predfrirr 14552  poxpOLD 14602  frxpOLD 14604  soseq 14608  axdenselem4 14691  axdenselem5 14692  nocvxminlem 14697  axfelem14 14712  elfuns 14774  fiiu 15052  vxveqv 15067  fvsnn 15162  unprj 15250  dstr 15255  dffprod 15409  nelioo5 15609  efilcp2 15692  cnfilca 15693  rcfpfillem2 15695  bwt2 15738  iintlem1 15802  mamb 15824  tarsuc2 16055  isplibg3 16123  ordisoOLD 16198  ordtypelem5OLD 16203  ordtypelem6OLD 16204  ordtypelem7OLD 16205  ordtypeOLD 16206  omsubssOLD 16217  omsubdmssOLD 16219  hscptsscld 16258  compfipin0lem 16259  compfipin0 16260  alexsublem2 16262  alexsublem3 16263  alexsublem4 16264  connsub 16267  reconnlem4 16273  t0dist 16365  ist1-2 16366  ist1-3 16367  t1sep 16370  fbasfip 16380  filfinnfr 16385  filssufil 16395  ufileu 16397  ufinffr 16402  flimcls 16412  flimfcls 16437  flimfnfcls 16439  filnet 16469  inficl 16581  supubt 16587  zornn0 16588  infmrlb 16589  infmrgelb 16590  frfiOLD 16595  frminexOLD 16597  fsumlt1 16655  heiborlem20 16798  smprngpr 17024  sbcnel12g 17232  rusbcALT 17234  compab 17242  xrltneNEW 17258  en3lpVD 17503  opltcon3b 17598  cvrfval 17660  cvrval 17661  cvrnbtwn 17663  cvrval2 17665  cvrnbtwn2 17666  cvrnbtwn3 17667  cvrcon3b 17668  cvrnbtwn4 17670  atnltOLD 17692  atnlt 17709  iscvlat 17720  cvlexch1 17725  hlsuprexch 17775  hlrelat5 17796  hlrelat2 17798  cvrval5 17810  3dimlem1 17854  3dim1lem5 17862  3dim2 17864  3dim3 17865  llnnlt 17956  islpln5 17966  lplni2 17968  lvolex3 17969  lplnnle2at 17973  islpln2a 17980  lplnrib 17983  lplnexlln 17996  lplnnlt 17997  lvoli3 18009  islvol5 18011  lvoli2 18013  lvolnle3at 18014  islvol2a 18024  4atlem11 18041  lvolnlt 18050  dalawlem15 18317  lautcvr 18446  ltrnfset 18470  ltrnset 18471  ltrnu 18474  trlfset 18505  trlset 18506  trlval2 18508  trlval2OLD 18509  4atexlemex2 18541  cdlemd6 18571  cdleme0nex 18661  cdleme18d 18666  cdleme25b 18726  cdleme25cv 18730  cdleme29b 18748  cdleme31fv 18764  cdleme31fv2 18767  cdlemefrs29bpre0 18770  cdlemefrs32fva 18774  cdlemefr32sn2aw 18778  cdlemefr29bpre0 18780  cdlemefr29cl 18781  cdlemefr32fva 18783  cdlemefr32fva1 18784  cdlemefs32sn1aw 18788  cdleme32fva 18812  cdleme32fvawOLD 18814  cdleme32fvaw 18815  cdleme35sn3a 18835  cdleme40vOLD 18846  cdleme40v 18848  cdleme42b 18857  cdleme46f2g2 18874  cdleme46f2g1 18875  cdleme48gfv 18922  cdlemg1fvawlem 18952  cdlemg1cex 18963  cdlemgfvawOLD 18964  cdlemg6d 19001

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 220

Copyright terms: Public domain