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  2021  sbco4  2059  elsb1  2208  elsb2  2209  abeq1i  2342  cbvabw  2353  r19.41  2687  rexcom4a  2826  moeq  2980  mosubt  2982  2reuswapdc  3009  nfcdeq  3027  sbcid  3046  sbcco2  3053  sbc7  3057  sbcie2g  3064  eqsbc1  3070  sbcralt  3107  sbcrext  3108  cbvralcsf  3189  cbvrexcsf  3190  cbvrabcsf  3192  abss  3295  ssab  3296  difrab  3480  abn0m  3519  prsspw  3847  disjnim  4077  brab1  4135  unopab  4167  exss  4318  uniuni  4547  elvvv  4788  eliunxp  4868  ralxp  4872  rexxp  4873  opelco  4901  reldm0  4948  resieq  5022  resiexg  5057  iss  5058  imai  5091  cnvsym  5119  intasym  5120  asymref  5121  codir  5124  poirr2  5128  rninxp  5179  cnvsom  5279  funopg  5359  fin  5522  f1cnvcnv  5553  fndmin  5754  resoprab  6119  mpo2eqb  6133  ov6g  6162  offval  6245  dfopab2  6354  dfoprab3s  6355  fmpox  6367  spc2ed  6400  brtpos0  6420  dftpos3  6430  tpostpos  6432  ercnv  6725  xpcomco  7012  xpassen  7016  phpm  7054  ctssdccl  7312  elni2  7536  elfz2nn0  10349  elfzmlbp  10369  clim0  11865  nnwosdc  12630  isstructim  13116  xpscf  13450  srgrmhm  14028  ntreq0  14882  cnmptcom  15048  dedekindicclemicc  15382