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 671  pm5.24 672  xor2 673  nicodraw 952  equsb3lem 1329  elsb3 1331  sbelx 1344  euan 1428  2mos 1448  abeq1i 1571  necon1bbii 1617  r19.41v 1763  reeanv 1778  moeq 1920  2reuswap 1937  elabs2 1964  abss 2117  ssab 2118  uniiunlem 2132  difrab 2273  n0 2289  vdif0 2328  difin0ss 2332  ssiin 2599  unopab 2679  axrep5 2698  axsep 2702  intexab 2731  uniuni 2880  reusn 2892  reuxfr 2904  dfwe2 2935  wefrc 2943  ordelord 2970  onminex 3020  orduniorsuc 3087  dfom2 3133  tfinds2 3165  brinxp2 3231  dmsnop 3328  resieq 3376  resiexg 3396  iss 3397  imai 3417  intasym 3438  asymref 3439  cnvi 3447  dffun3 3527  funopg 3547  fcoi2 3646  fin 3651  f1cnv 3666  funimass4 3763  fvreseq 3799  fopab3 3826  fnressn 3837  fopabap 3841  abrexexlem2 3859  imaiun 3864  tz7.48lem 3955  resoprab 4009  oprabval6g 4032  foprab2 4119  ecelqsdm 4299  xpassen 4441  php 4513  infeq5 4621  rankeq0 4696  rankxplim 4712  scott0s 4719  aceq1 4729  aceq5lem1 4735  aceq5lem2 4736  kmlem3 4767  kmlem8 4772  kmlem16 4780  alephval2 4902  cflem 4905  cf0 4910  ltpiord 5015  distrlem5pr 5131  psslinpr 5135  reclem1pr 5156  reclem2pr 5157  suppsr3 5224  ssxr 5540  ltmullem 5640  div11 5764  posex 5908  infm3 6054  infmsup 6068  supxrre 6083  elnnz1 6155  ioo0t 6368  nnwos 6460  sqeqor 6647  discrlem3 6658  sqr2irrlem1 6724  cjreb 6781  cau3ir 6915  sumex 6981  climuz0 7108  cvgcmpub 7185  isumnn0nna 7208  isummulc1a 7214  efcnlem1 7419  tgss3t 7638  blfval2 7836  lmfval 7925  bcthlem7 8005  ghgrpilem2 8134  nvvcop 8213  sspval 8382  lnon0 8458  efifolem2 8723  efif1lem5 8734  efif1lem7 8736  pjpj0 9255  spansncv 9597  pjssm 9626  nmlnopgt0 9922  large 10194  cvexchlem 10295  cnfilca 10583  cnfilcaOLD 10584

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