Theorem bitr3i 186

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

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 132	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 184	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrri  207  3bitr3i  210  3bitr3ri  211  anandi  590  anandir  591  xchnxbi  680  orordi  773  orordir  774  sbco3v  1969  sbco4  2007  elsb1  2155  elsb2  2156  abeq1i  2289  cbvabw  2300  r19.41  2632  rexcom4a  2762  moeq  2913  mosubt  2915  2reuswapdc  2942  nfcdeq  2960  sbcid  2979  sbcco2  2986  sbc7  2990  sbcie2g  2997  eqsbc1  3003  sbcralt  3040  sbcrext  3041  cbvralcsf  3120  cbvrexcsf  3121  cbvrabcsf  3123  abss  3225  ssab  3226  difrab  3410  abn0m  3449  prsspw  3766  disjnim  3995  brab1  4051  unopab  4083  exss  4228  uniuni  4452  elvvv  4690  eliunxp  4767  ralxp  4771  rexxp  4772  opelco  4800  reldm0  4846  resieq  4918  resiexg  4953  iss  4954  imai  4985  cnvsym  5013  intasym  5014  asymref  5015  codir  5018  poirr2  5022  rninxp  5073  cnvsom  5173  funopg  5251  fin  5403  f1cnvcnv  5433  fndmin  5624  resoprab  5971  mpo2eqb  5984  ov6g  6012  offval  6090  dfopab2  6190  dfoprab3s  6191  fmpox  6201  spc2ed  6234  brtpos0  6253  dftpos3  6263  tpostpos  6265  ercnv  6556  xpcomco  6826  xpassen  6830  phpm  6865  ctssdccl  7110  elni2  7313  elfz2nn0  10112  elfzmlbp  10132  clim0  11293  nnwosdc  12040  isstructim  12476  xpscf  12766  srgrmhm  13177  ntreq0  13635  cnmptcom  13801  dedekindicclemicc  14113