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  580  anandir  581  xchnxbi  670  orordi  763  orordir  764  sbco3v  1957  sbco4  1995  elsb1  2143  elsb2  2144  abeq1i  2278  cbvabw  2289  r19.41  2621  rexcom4a  2750  moeq  2901  mosubt  2903  2reuswapdc  2930  nfcdeq  2948  sbcid  2966  sbcco2  2973  sbc7  2977  sbcie2g  2984  eqsbc1  2990  sbcralt  3027  sbcrext  3028  cbvralcsf  3107  cbvrexcsf  3108  cbvrabcsf  3110  abss  3211  ssab  3212  difrab  3396  abn0m  3434  prsspw  3745  disjnim  3973  brab1  4029  unopab  4061  exss  4205  uniuni  4429  elvvv  4667  eliunxp  4743  ralxp  4747  rexxp  4748  opelco  4776  reldm0  4822  resieq  4894  resiexg  4929  iss  4930  imai  4960  cnvsym  4987  intasym  4988  asymref  4989  codir  4992  poirr2  4996  rninxp  5047  cnvsom  5147  funopg  5222  fin  5374  f1cnvcnv  5404  fndmin  5592  resoprab  5938  mpo2eqb  5951  ov6g  5979  offval  6057  dfopab2  6157  dfoprab3s  6158  fmpox  6168  spc2ed  6201  brtpos0  6220  dftpos3  6230  tpostpos  6232  ercnv  6522  xpcomco  6792  xpassen  6796  phpm  6831  ctssdccl  7076  elni2  7255  elfz2nn0  10047  elfzmlbp  10067  clim0  11226  nnwosdc  11972  isstructim  12408  ntreq0  12772  cnmptcom  12938  dedekindicclemicc  13250