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 578  nan 688  pm4.83 739  pm5.7 745  nicodraw 950  19.12vv 1300  2exsb 1349  2eu4 1450  cvjust 1469  cla42gv 1861  cla43gv 1863  sbcralt 1986  sbcralgf 1988  ss2rab 2119  ddif 2165  difab 2265  disj 2307  ssindif0 2318  iunss 2586  ssiun 2587  iunn0 2602  unopab 2674  axrep5 2693  sbcsng 2748  eqvinop 2786  pwssun 2822  pwexb 2903  suceloni 3057  reldm0 3326  iss 3389  dfima2 3397  imadmrn 3406  asymref2 3432  intirr 3433  ssrnres 3473  cnvpo 3514  fun11 3554  fununi 3555  funcnvuni 3556  tz6.12-2 3730  fsn 3825  fconstfv 3840  imaiun 3855  funiunfv 3857  abianfp 3953  eloprabg 3998  funoprabg 4001  dfer2 4252  map1 4417  xpsnen 4421  mapxpen 4481  pwen 4489  zfregcl 4575  zfregs 4627  rankbnd 4683  rankbnd2 4684  rankxplim2 4693  rankxplim3 4694  aceq3lem 4712  aceq3 4713  aceq5lem2 4716  aceq5lem5 4719  aceq5 4720  ac9s 4744  kmlem14 4758  kmlem15 4759  kmlem16 4760  brdom3 4781  suplem2pr 5142  supsrlem3 5207  lttri4t 5495  xrrebndt 5549  leneg 5586  lesub0 5594  nnunb 6025  uzwo3lem1 6172  elioo3g 6325  elfz2t 6412  cjreb 6724  cau3ir 6860  clmnns 7030  tgval2t 7567  0top 7585  subbas 7594  islp2 7697  lpbl 7832  lmbrnns 7894  bcthlem14 7962  bcthlem33 7981  pilem3 8611  sinhalfpilem 8617  shlesb1 9297  pjss2 9565  pjnel 9608  lnopcon 9901  lnfncon 9928  cnlnssadj 9951  pjin2 10059  cvnbtwn2t 10152  cvnbtwn4t 10154  mdsl1 10185  mdsl2 10186  hatomistic 10226  cdj3lem3b 10301  abfi 10385

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