Theorem bitr2 152

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 151	. 2 |- (ph <-> ch)
4	3	bicomi 150	1 |- (ch <-> ph)

Syntax hints:   <-> wb 127

This theorem is referenced by:  3bitr4r 159  pm2.85 439  nan 514  19.12vv 960  2eu4 1070  cla42gv 1399  zfrep3 1476  3sstr3 1538  ss2rab 1553  ddif 1597  difab 1693  disj 1733  ssindif0 1741  eqvinop 1901  pwssun 1917  pwexb 1963  iunss 2017  ssiun 2018  iunn0 2029  unopab 2121  poirr 2133  so 2152  suceloni 2314  cnvuni 2521  reldm0 2550  iss 2599  dfima2 2604  imadmrn 2610  intirr 2628  imaiun 2650  fununi 2705  funcnvuni 2706  tz6.12-2 2845  fsn 2895  fconstfv 2903  abianfp 3000  eloprabg 3035  er2 3201  map1 3335  xpsnen 3339  mapxpen 3390  pwen 3398  fiint 3445  zfregcl 3446  zfregs 3491  aceq3lem 3555  aceq3 3556  aceq5lem2 3559  aceq5lem3 3560  aceq5lem5 3562  aceq5 3563  kmlem15 3594  kmlem16 3595  suplem2pr 3956  supsrlem3 4021  posdif 4328  leneg 4331  lesub0 4341  subge0 4342  negne0 4379  nnunb 4520  elznn0 4576  uzwo3lem1 4614  sqr2irrlem4 4780  cjre 4811  shlesb1 5360  cmbr2 5505  pjss2 5571  pjin2 5647  cvnbtwn2t 5719  cvnbtwn4t 5721  hatomistic 5755  chrelat2 5758

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

metamath.org