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  2824  moeq  2978  mosubt  2980  2reuswapdc  3007  nfcdeq  3025  sbcid  3044  sbcco2  3051  sbc7  3055  sbcie2g  3062  eqsbc1  3068  sbcralt  3105  sbcrext  3106  cbvralcsf  3187  cbvrexcsf  3188  cbvrabcsf  3190  abss  3293  ssab  3294  difrab  3478  abn0m  3517  prsspw  3842  disjnim  4072  brab1  4130  unopab  4162  exss  4312  uniuni  4541  elvvv  4781  eliunxp  4860  ralxp  4864  rexxp  4865  opelco  4893  reldm0  4940  resieq  5014  resiexg  5049  iss  5050  imai  5083  cnvsym  5111  intasym  5112  asymref  5113  codir  5116  poirr2  5120  rninxp  5171  cnvsom  5271  funopg  5351  fin  5511  f1cnvcnv  5541  fndmin  5741  resoprab  6099  mpo2eqb  6113  ov6g  6142  offval  6224  dfopab2  6333  dfoprab3s  6334  fmpox  6344  spc2ed  6377  brtpos0  6396  dftpos3  6406  tpostpos  6408  ercnv  6699  xpcomco  6981  xpassen  6985  phpm  7023  ctssdccl  7274  elni2  7497  elfz2nn0  10304  elfzmlbp  10324  clim0  11791  nnwosdc  12555  isstructim  13041  xpscf  13375  srgrmhm  13952  ntreq0  14800  cnmptcom  14966  dedekindicclemicc  15300