Theorem bitr3i 173

Description: An inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

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

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 |- (ps <-> ph)
2	1	bicomi 170	. 2 |- (ph <-> ps)
3		bitr3i.2	. 2 |- (ps <-> ch)
4	2, 3	bitri 171	1 |- (ph <-> ch)

Syntax hints:   <-> wb 144

This theorem is referenced by:  3bitrri 176  3bitr3i 179  3bitr3ri 180  orordi 264  orordir 265  anabs5 496  anandi 513  anandir 514  xor 674  pm5.24 675  xor2 676  dn1 779  nic-axALT 970  equsb3lem 1368  elsb3 1370  sbelx 1383  euan 1467  2mos 1488  abeq1i 1614  necon1bbii 1661  r19.41v 1809  reeanv 1824  moeq 1966  2reuswap 1983  elabs2 2012  abss 2169  ssab 2170  uniiunlem 2184  difrab 2325  neq0 2342  vdif0 2381  difin0ss 2385  ssiin 2667  unopab 2753  axrep5 2772  axsep 2776  intexab 2805  wefrc 2970  ordelord 2997  uniuni 3104  reusn 3115  reuxfr 3127  dfwe2 3140  onminex 3164  orduniorsuc 3184  tfinds2 3216  dfom2 3220  elvvv 3314  brinxp2 3317  resieq 3463  resiexg 3486  iss 3487  imai 3509  intasym 3530  asymref 3531  cnvi 3539  dffun3 3632  funopg 3652  fcoi2 3753  fin 3758  f1cnv 3773  funimass4 3874  fopab3 3940  fnressn 3951  fopabap 3955  abrexexlem2 3973  imaiun 3978  resoprab 4069  oprabval6g 4093  foprab2 4181  fsplit 4204  tz7.48lem 4256  ecelqsdm 4440  xpassen 4582  php 4660  infeq5 4766  rankeq0 4842  rankxplim 4858  scott0s 4865  aceq1 4875  aceq5lem1 4881  aceq5lem2 4882  kmlem3 4913  kmlem8 4918  kmlem16 4926  alephval2 5052  cflem 5055  cf0 5060  ltpiord 5169  distrlem5pr 5285  psslinpr 5289  reclem1pr 5310  reclem2pr 5311  suppsr3 5378  ssxr 5694  ltmullem 5794  div11i 5903  posexi 6053  infm3 6222  infmsup 6236  supxrre 6251  elnnz1 6323  ioo0 6494  nnwos 6587  sqeqori 6844  discrlem3 6859  sqr2irrlem1 6925  cjrebi 6982  cau3iri 7118  sumex 7184  climuz0i 7311  cvgcmpubi 7389  isumnn0nnai 7412  isummulc1ai 7418  efcnlem1 7627  tgss3 7850  blfval2 8046  lmfval 8136  bcthlem7 8216  ghgrpilem2 8375  nvvcop 8460  sspval 8636  lnon0 8713  efifolem2 8995  efif1lem5 9006  efif1lem7 9008  pjpj0i 9531  spansncvi 9875  pjssmii 9904  nmlnopgt0i 10201  largei 10475  cvexchlem 10576  cnfilca 11088  fiuni 11420  onsdom 11437  neibastop2lem1 11580  topmtcl 11586  topjoin 11588  isufil2 11650  ufileu 11658  hausfillim 11685  fcluscf 11724  flimfnfcls 11727  filnetlem4 11766  inixp 11820  sdc 11877  mettrifi 11912  totbndbnd 12000  heiborlem24 12034

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 145

Copyright terms: Public domain