Theorem bitr2i 191

Description: An inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

Ref	Expression
bitr2i	|- (ch <-> ph)

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 |- (ph <-> ps)
2		bitr2i.2	. . 3 |- (ps <-> ch)
3	1, 2	bitri 190	. 2 |- (ph <-> ch)
4	3	bicomi 189	1 |- (ch <-> ph)

Syntax hints:   <-> wb 163

This theorem is referenced by:  3bitrri 195  3bitr2ri 197  3bitr4ri 201  pm2.85 639  nan 753  pm4.83 812  pm5.7 818  nic-justim 1232  nic-justneg 1233  19.12vv 1681  19.12vvOLD 1682  2exsb 1742  2eu4 1856  cvjust 1879  cla42gv 2367  cla43gv 2369  reuind 2450  sbcralt 2527  sbcralgf 2529  ss2rab 2683  ddif 2737  unass 2759  undi 2840  difabOLD 2864  disj 2914  ssindif0 2927  sbcsngOLD 3087  pwsnALT 3173  iunssOLD 3292  ssiunOLD 3294  iunn0OLD 3316  iinrab2 3319  brab1 3384  unopab 3410  truni 3425  axrep5 3433  eqvinop 3536  pwssun 3578  pwexb 3852  suceloni 3894  elvvv 4054  dmun 4163  reldm0 4176  issOLD 4255  dfima2OLD 4266  imadmrn 4277  asymref2OLD 4311  intirrOLD 4313  ssrnres 4354  dmsnn0 4362  coundi 4396  coundir 4398  cnvpo 4427  fun11 4480  fununi 4481  funcnvuni 4482  tz6.12-2 4696  dffv2 4734  eufnfv 4771  fsn 4807  fconstfv 4825  imaiun 4840  funiunfv 4842  eloprabg 4936  funoprabg 4939  fparlem1 5081  fparlem2 5082  fsplit 5086  abianfp 5171  dfer2 5319  map1 5489  xpsnen 5494  mapxpen 5589  pwen 5597  ordtypelem6 5689  zfregcl 5697  zfregs 5754  rankbnd 5814  rankbnd2 5815  rankxplim2 5824  rankxplim3 5825  aceq3lem 5894  aceq3 5895  aceq5lem2 5898  aceq5lem5 5901  aceq5 5902  ac9s 5926  kmlem14 5940  kmlem15 5941  kmlem16 5942  brdom3 5963  suplem2pr 6314  supsrlem3 6379  lttri4OLD 6685  xrrebnd 6743  lenegi 6784  lesub0iOLD 6793  nnunb 7279  uzwo3lem1 7429  elioo3g 7547  elfz2 7642  fzsuc 7678  cjrebi 8031  cau3iri 8167  clmnnsi 8344  tgval2 8887  0top 8905  subbas 8914  islp2 9023  lpbl 9157  lmbrnns 9220  bcthlem14 9290  bcthlem33 9309  gapm 9462  pilem3 10022  sinhalfpilem 10028  abfi 10215  filrn 10293  shlesb1i 10992  pjss2i 11260  pjneli 11303  lnopconi 11600  lnfnconi 11627  cnlnssadj 11650  pjin2i 11766  cvnbtwn2 11859  cvnbtwn4 11861  mdsl1i 11893  mdsl2i 11894  hatomistici 11934  cdj3lem3b 12012  bnj35 12404  bnj63 12432  bnj112 12457  bnj142 12474  bnj168 12496  bnj153 13247  bnj578 13291  bnj605 13292  bnj607 13304  bnj986 13360  truniOLD 13792  3or6 13804  19.12b 13868  soseq 13955  axfelem11 14041  negcmpprcal1 14275  albineal 14323  cnvresima 15359  trer 15361  ioodisj 15364  inficlALT 15372  ordtypelem6OLD 15380  uncomp 15433  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsub 15441  isfne3 15482  locfincomp 15514  neibastop2lem3 15521  neibastop2lem4 15522  ist1-3 15543  opnfbas 15557  filssufillem 15570  ufileu 15573  filufint 15574  filcon 15580  fcluscomp 15621  filnetlem1 15640  rabeq0 15666  oprabrexex2 15709  pi1bvalqs 16091  iotasbc2 16384

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 164

Copyright terms: Public domain