Theorem bitr3 175

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 172	. 2 |- (ph <-> ps)
3		bitr3.2	. 2 |- (ps <-> ch)
4	2, 3	bitr 173	1 |- (ph <-> ch)

Syntax hints:   <-> wb 146

This theorem is referenced by:  3bitrr 178  3bitr3 181  3bitr3r 182  orordi 266  orordir 267  anabs5 493  anandi 510  anandir 511  xor 670  pm5.24 671  xor2 672  nicodraw 950  equsb3lem 1327  elsb3 1329  sbelx 1342  euan 1426  2mos 1446  abeq1i 1568  necon1bbii 1614  r19.41v 1760  reeanv 1775  moeq 1916  2reuswap 1933  elabs2 1960  abss 2113  ssab 2114  uniiunlem 2128  difrab 2269  n0 2285  vdif0 2324  difin0ss 2328  ssiin 2594  unopab 2674  axrep5 2693  axsep 2697  intexab 2726  uniuni 2875  reusn 2887  reuxfr 2899  dfwe2 2930  wefrc 2938  ordelord 2965  onminex 3015  orduniorsuc 3082  dfom2 3128  tfinds2 3160  brinxp2 3226  dmsnop 3323  resieq 3368  resiexg 3388  iss 3389  imai 3409  intasym 3430  asymref 3431  cnvi 3439  dffun3 3519  funopg 3539  fcoi2 3637  fin 3642  f1cnv 3657  funimass4 3754  fvreseq 3790  fopab3 3817  fnressn 3828  fopabap 3832  abrexexlem2 3850  imaiun 3855  tz7.48lem 3946  resoprab 4000  oprabval6g 4023  foprab2 4109  ecelqsdm 4289  xpassen 4427  php 4499  infeq5 4601  rankeq0 4676  rankxplim 4692  scott0s 4699  aceq1 4709  aceq5lem1 4715  aceq5lem2 4716  kmlem3 4747  kmlem8 4752  kmlem16 4760  alephval2 4882  cflem 4885  cf0 4890  ltpiord 4995  distrlem5pr 5111  psslinpr 5115  reclem1pr 5136  reclem2pr 5137  suppsr3 5204  ssxr 5521  ltmullem 5622  div11 5728  posex 5864  infm3 6009  infmsup 6023  supxrre 6038  elnnz1 6110  ioo0t 6313  nnwos 6400  sqeqor 6586  discrlem3 6596  nn0opth 6604  sqr2irrlem1 6662  cjreb 6724  absgt0 6786  cau3ir 6860  sumex 6927  climuz0 7053  cvgcmpub 7129  isumnn0nna 7151  isummulc1a 7157  efcnlem1 7367  tgss3t 7588  blfval2 7788  lmfval 7877  bcthlem7 7955  ghgrpilem2 8086  nvvcop 8165  sspval 8329  efifolem2 8657  efif1lem5 8668  efif1lem7 8670  pjpj0 9193  spansncv 9537  pjssm 9566  nmlnopgt0 9860  large 10132  cvexchlem 10232  cnfilca 10487

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