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  592  anandir  593  xchnxbi  684  orordi  778  orordir  779  sbco3v  2020  sbco4  2058  elsb1  2207  elsb2  2208  abeq1i  2341  cbvabw  2352  r19.41  2686  rexcom4a  2825  moeq  2979  mosubt  2981  2reuswapdc  3008  nfcdeq  3026  sbcid  3045  sbcco2  3052  sbc7  3056  sbcie2g  3063  eqsbc1  3069  sbcralt  3106  sbcrext  3107  cbvralcsf  3188  cbvrexcsf  3189  cbvrabcsf  3191  abss  3294  ssab  3295  difrab  3479  abn0m  3518  prsspw  3846  disjnim  4076  brab1  4134  unopab  4166  exss  4317  uniuni  4546  elvvv  4787  eliunxp  4867  ralxp  4871  rexxp  4872  opelco  4900  reldm0  4947  resieq  5021  resiexg  5056  iss  5057  imai  5090  cnvsym  5118  intasym  5119  asymref  5120  codir  5123  poirr2  5127  rninxp  5178  cnvsom  5278  funopg  5358  fin  5520  f1cnvcnv  5550  fndmin  5750  resoprab  6112  mpo2eqb  6126  ov6g  6155  offval  6238  dfopab2  6347  dfoprab3s  6348  fmpox  6360  spc2ed  6393  brtpos0  6413  dftpos3  6423  tpostpos  6425  ercnv  6718  xpcomco  7005  xpassen  7009  phpm  7047  ctssdccl  7301  elni2  7524  elfz2nn0  10337  elfzmlbp  10357  clim0  11836  nnwosdc  12600  isstructim  13086  xpscf  13420  srgrmhm  13997  ntreq0  14846  cnmptcom  15012  dedekindicclemicc  15346