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 951  19.12vv 1302  2exsb 1351  2eu4 1452  cvjust 1471  cla42gv 1863  cla43gv 1865  sbcralt 1988  sbcralgf 1990  ss2rab 2121  ddif 2167  difab 2267  disj 2309  ssindif0 2320  iunss 2588  ssiun 2589  iunn0 2604  unopab 2676  axrep5 2695  sbcsng 2750  eqvinop 2788  pwssun 2824  pwexb 2905  suceloni 3059  reldm0 3328  iss 3394  dfima2 3402  imadmrn 3411  asymref2 3437  intirr 3438  ssrnres 3478  cnvpo 3519  fun11 3559  fununi 3560  funcnvuni 3561  tz6.12-2 3736  fsn 3831  fconstfv 3846  imaiun 3861  funiunfv 3863  abianfp 3959  eloprabg 4004  funoprabg 4007  dfer2 4259  map1 4424  xpsnen 4428  mapxpen 4488  pwen 4496  zfregcl 4582  zfregs 4634  rankbnd 4690  rankbnd2 4691  rankxplim2 4700  rankxplim3 4701  aceq3lem 4719  aceq3 4720  aceq5lem2 4723  aceq5lem5 4726  aceq5 4727  ac9s 4751  kmlem14 4765  kmlem15 4766  kmlem16 4767  brdom3 4788  suplem2pr 5149  supsrlem3 5214  lttri4t 5502  xrrebndt 5555  leneg 5592  lesub0 5600  nnunb 6031  uzwo3lem1 6178  elioo3g 6335  elfz2t 6422  cjreb 6740  cau3ir 6881  clmnns 7052  tgval2t 7596  0top 7614  subbas 7623  islp2 7726  lpbl 7863  lmbrnns 7925  bcthlem14 7995  bcthlem33 8014  pilem3 8656  sinhalfpilem 8662  shlesb1 9347  pjss2 9616  pjnel 9659  lnopcon 9954  lnfncon 9981  cnlnssadj 10004  pjin2 10112  cvnbtwn2t 10205  cvnbtwn4t 10207  mdsl1 10239  mdsl2 10240  hatomistic 10280  cdj3lem3b 10358  abfi 10442

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