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-1 5  ax-2 6  ax-mp 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  562  anandir  563  xchnxbi  652  orordi  745  orordir  746  sbco3v  1916  elsb3  1925  elsb4  1926  sbco4  1956  abeq1i  2224  r19.41  2558  rexcom4a  2679  moeq  2826  mosubt  2828  2reuswapdc  2855  nfcdeq  2873  sbcid  2891  sbcco2  2898  sbc7  2902  sbcie2g  2908  eqsbc3  2914  sbcralt  2951  sbcrext  2952  cbvralcsf  3026  cbvrexcsf  3027  cbvrabcsf  3029  abss  3130  ssab  3131  difrab  3314  abn0m  3352  prsspw  3656  disjnim  3884  brab1  3938  unopab  3965  exss  4107  uniuni  4330  elvvv  4560  eliunxp  4636  ralxp  4640  rexxp  4641  opelco  4669  reldm0  4715  resieq  4785  resiexg  4820  iss  4821  imai  4851  cnvsym  4878  intasym  4879  asymref  4880  codir  4883  poirr2  4887  rninxp  4938  cnvsom  5038  funopg  5113  fin  5265  f1cnvcnv  5295  fndmin  5479  resoprab  5819  mpo2eqb  5832  ov6g  5860  offval  5941  dfopab2  6038  dfoprab3s  6039  fmpox  6049  spc2ed  6081  brtpos0  6100  dftpos3  6110  tpostpos  6112  ercnv  6401  xpcomco  6670  xpassen  6674  phpm  6709  ctssdccl  6945  elni2  7063  elfz2nn0  9778  elfzmlbp  9795  clim0  10939  isstructim  11809  ntreq0  12137  cnmptcom  12302