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 579  nan 689  pm4.83 740  pm5.7 746  nicodraw 952  19.12vv 1302  2exsb 1351  2eu4 1452  cvjust 1471  cla42gv 1865  cla43gv 1867  sbcralt 1990  sbcralgf 1992  ss2rab 2123  ddif 2169  difab 2269  disj 2311  ssindif0 2322  pwsnALT 2501  iunss 2591  ssiun 2592  iunn0 2607  unopab 2679  axrep5 2698  sbcsng 2753  eqvinop 2791  pwssun 2827  pwexb 2908  suceloni 3062  reldm0 3331  iss 3397  dfima2 3405  imadmrn 3414  asymref2 3440  intirr 3441  ssrnres 3481  cnvpo 3522  fun11 3562  fununi 3563  funcnvuni 3564  tz6.12-2 3739  fsn 3834  fconstfv 3849  imaiun 3864  funiunfv 3866  abianfp 3962  eloprabg 4007  funoprabg 4010  dfer2 4262  map1 4430  xpsnen 4435  mapxpen 4495  pwen 4503  zfregcl 4595  zfregs 4647  rankbnd 4703  rankbnd2 4704  rankxplim2 4713  rankxplim3 4714  aceq3lem 4732  aceq3 4733  aceq5lem2 4736  aceq5lem5 4739  aceq5 4740  ac9s 4764  kmlem14 4778  kmlem15 4779  kmlem16 4780  brdom3 4801  suplem2pr 5162  supsrlem3 5227  lttri4t 5515  xrrebndt 5568  leneg 5604  lesub0 5612  nnunb 6070  uzwo3lem1 6216  elioo3g 6380  elfz2t 6472  cjreb 6781  cau3ir 6915  clmnns 7084  tgval2t 7617  0top 7635  subbasOLD 7644  islp2 7747  lpbl 7880  lmbrnns 7942  bcthlem14 8012  bcthlem33 8031  pilem3 8673  sinhalfpilem 8679  shlesb1 9359  pjss2 9625  pjnel 9668  lnopcon 9963  lnfncon 9990  cnlnssadj 10013  pjin2 10121  cvnbtwn2t 10214  cvnbtwn4t 10216  mdsl1 10248  mdsl2 10249  hatomistic 10289  cdj3lem3b 10367  abfi 10451  abfiOLD 10452

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