Theorem bitr2 174

Description: An inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

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

Proof of Theorem bitr2

Step	Hyp	Ref	Expression
1		bitr2.1	. . 3 |- (ph <-> ps)
2		bitr2.2	. . 3 |- (ps <-> ch)
3	1, 2	bitr 173	. 2 |- (ph <-> ch)
4	3	bicomi 172	1 |- (ch <-> ph)

Syntax hints:   <-> wb 146

This theorem is referenced by:  3bitrr 178  3bitr2r 180  3bitr4r 184  pm2.85 581  nan 691  pm4.83 742  pm5.7 748  nicodraw 954  19.12vv 1304  2exsb 1353  2eu4 1455  cvjust 1474  cla42gv 1868  cla43gv 1870  sbcralt 1993  sbcralgf 1995  ss2rab 2126  ddif 2172  difab 2272  disj 2315  ssindif0 2326  pwsnALT 2505  iunss 2595  ssiun 2596  iunn0 2612  unopab 2684  axrep5 2703  sbcsng 2759  eqvinop 2797  pwssun 2833  pwexb 2914  suceloni 3068  reldm0 3337  iss 3403  dfima2 3411  imadmrn 3420  asymref2 3446  intirr 3447  ssrnres 3487  cnvpo 3528  fun11 3568  fununi 3569  funcnvuni 3570  tz6.12-2 3745  fsn 3840  fconstfv 3855  imaiun 3870  funiunfv 3872  abianfp 3968  eloprabg 4013  funoprabg 4016  dfer2 4268  map1 4436  xpsnen 4441  mapxpen 4501  pwen 4509  zfregcl 4604  zfregs 4657  rankbnd 4713  rankbnd2 4714  rankxplim2 4723  rankxplim3 4724  aceq3lem 4742  aceq3 4743  aceq5lem2 4746  aceq5lem5 4749  aceq5 4750  ac9s 4774  kmlem14 4788  kmlem15 4789  kmlem16 4790  brdom3 4811  suplem2pr 5174  supsrlem3 5239  lttri4t 5527  xrrebndt 5580  leneg 5616  lesub0 5624  nnunb 6072  uzwo3lem1 6218  elioo3g 6381  elfz2t 6473  cjreb 6781  cau3ir 6915  clmnns 7084  tgval2t 7616  0top 7634  islp2 7744  lpbl 7877  lmbrnns 7939  bcthlem14 8009  bcthlem33 8028  pilem3 8668  sinhalfpilem 8674  shlesb1 9354  pjss2 9620  pjnel 9663  lnopcon 9958  lnfncon 9985  cnlnssadj 10008  pjin2 10116  cvnbtwn2t 10209  cvnbtwn4t 10211  mdsl1 10243  mdsl2 10244  hatomistic 10284  cdj3lem3b 10362  abfi 10443

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

Copyright terms: Public domain