Theorem bitr3 153

Description: An inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

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

Proof of Theorem bitr3

Step	Hyp	Ref	Expression
1		bitr3.1	. . 3 |- (ps <-> ph)
2	1	bicomi 150	. 2 |- (ph <-> ps)
3		bitr3.2	. 2 |- (ps <-> ch)
4	2, 3	bitr 151	1 |- (ph <-> ch)

Syntax hints:   <-> wb 127

This theorem is referenced by:  3bitr3 156  3bitr3r 157  orordi 222  orordir 223  anabs5 375  anandi 392  anandir 393  xor 500  sb5y 883  sbelx 994  euanv 1053  2eu5 1071  cleqabri 1177  sbabel 1189  r19.41v 1302  reeanv 1316  2reuswap 1341  moeq 1431  elabs2 1457  zfrep3 1476  zfaus 1480  sspsstri 1572  reuxfr 1580  difrab 1695  vdif0 1749  difin0ss 1753  intexab 1987  dfiin2 2015  ssiin 2024  unopab 2121  poirr 2133  dfwe2 2187  wefrc 2195  ordelord 2221  ordtri3or 2230  onminex 2275  dfom2 2374  tfinds2 2405  dmopab2 2541  dmsnop 2547  reldm0 2550  iss 2599  imai 2613  eliniseg 2618  intasym 2627  cnvi 2634  imaiun 2650  dmco2 2673  dffun3 2675  funcnv2 2702  fununi 2705  fcoi2 2766  fin 2770  f1cnv 2782  fvreseq 2882  fsn 2895  fnressn 2897  abrexexlem2 2911  iinon 2948  tz7.48lem 2993  fnoprval 3042  ecelqsdm 3235  xpassen 3344  php 3409  inf5 3472  scott0s 3544  aceq1 3552  aceq5lem1 3558  aceq5lem2 3559  kmlem3 3582  kmlem4 3583  kmlem11 3590  kmlem13 3592  kmlem14 3593  kmlem15 3594  kmlem16 3595  cflem 3700  cf0 3705  ltpiord 3809  distrlem5pr 3925  psslinpr 3929  ltexprlem4 3939  reclem1pr 3950  reclem2pr 3951  suppsr3 4018  div11 4252  ltmullem 4337  lesub0 4341  elnnz1 4581  nnwos 4610  discrlem3 4715  sqr2irrlem1 4777  cjre 4811  absgt0 4842  pjthu 5241  pjthu2 5242  pjpj0 5259  shne0 5372  spansncv 5542  pjssm 5572  pjnel 5665  large 5700  chrelat2 5758  cvexchlem 5759

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