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  594  anandir  595  xchnxbi  686  orordi  780  orordir  781  sbco3v  2022  sbco4  2060  elsb1  2209  elsb2  2210  abeq1i  2343  cbvabw  2354  r19.41  2688  rexcom4a  2827  moeq  2981  mosubt  2983  2reuswapdc  3010  nfcdeq  3028  sbcid  3047  sbcco2  3054  sbc7  3058  sbcie2g  3065  eqsbc1  3071  sbcralt  3108  sbcrext  3109  cbvralcsf  3190  cbvrexcsf  3191  cbvrabcsf  3193  abss  3296  ssab  3297  difrab  3481  abn0m  3520  prsspw  3848  disjnim  4078  brab1  4136  unopab  4168  exss  4319  uniuni  4548  elvvv  4789  eliunxp  4869  ralxp  4873  rexxp  4874  opelco  4902  reldm0  4949  resieq  5023  resiexg  5058  iss  5059  imai  5092  cnvsym  5120  intasym  5121  asymref  5122  codir  5125  poirr2  5129  rninxp  5180  cnvsom  5280  funopg  5360  fin  5523  f1cnvcnv  5553  fndmin  5754  resoprab  6116  mpo2eqb  6130  ov6g  6159  offval  6242  dfopab2  6351  dfoprab3s  6352  fmpox  6364  spc2ed  6397  brtpos0  6417  dftpos3  6427  tpostpos  6429  ercnv  6722  xpcomco  7009  xpassen  7013  phpm  7051  ctssdccl  7309  elni2  7533  elfz2nn0  10346  elfzmlbp  10366  clim0  11845  nnwosdc  12609  isstructim  13095  xpscf  13429  srgrmhm  14006  ntreq0  14855  cnmptcom  15021  dedekindicclemicc  15355