Theorem bitr3i 185

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

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrri  206  3bitr3i  209  3bitr3ri  210  anandi  579  anandir  580  xchnxbi  669  orordi  762  orordir  763  sbco3v  1940  elsb3  1949  elsb4  1950  sbco4  1980  abeq1i  2249  cbvabw  2260  r19.41  2584  rexcom4a  2705  moeq  2854  mosubt  2856  2reuswapdc  2883  nfcdeq  2901  sbcid  2919  sbcco2  2926  sbc7  2930  sbcie2g  2937  eqsbc3  2943  sbcralt  2980  sbcrext  2981  cbvralcsf  3057  cbvrexcsf  3058  cbvrabcsf  3060  abss  3161  ssab  3162  difrab  3345  abn0m  3383  prsspw  3687  disjnim  3915  brab1  3970  unopab  4002  exss  4144  uniuni  4367  elvvv  4597  eliunxp  4673  ralxp  4677  rexxp  4678  opelco  4706  reldm0  4752  resieq  4824  resiexg  4859  iss  4860  imai  4890  cnvsym  4917  intasym  4918  asymref  4919  codir  4922  poirr2  4926  rninxp  4977  cnvsom  5077  funopg  5152  fin  5304  f1cnvcnv  5334  fndmin  5520  resoprab  5860  mpo2eqb  5873  ov6g  5901  offval  5982  dfopab2  6080  dfoprab3s  6081  fmpox  6091  spc2ed  6123  brtpos0  6142  dftpos3  6152  tpostpos  6154  ercnv  6443  xpcomco  6713  xpassen  6717  phpm  6752  ctssdccl  6989  elni2  7115  elfz2nn0  9885  elfzmlbp  9902  clim0  11047  isstructim  11962  ntreq0  12290  cnmptcom  12456  dedekindicclemicc  12768