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  590  anandir  591  xchnxbi  681  orordi  774  orordir  775  sbco3v  1988  sbco4  2026  elsb1  2174  elsb2  2175  abeq1i  2308  cbvabw  2319  r19.41  2652  rexcom4a  2787  moeq  2939  mosubt  2941  2reuswapdc  2968  nfcdeq  2986  sbcid  3005  sbcco2  3012  sbc7  3016  sbcie2g  3023  eqsbc1  3029  sbcralt  3066  sbcrext  3067  cbvralcsf  3147  cbvrexcsf  3148  cbvrabcsf  3150  abss  3253  ssab  3254  difrab  3438  abn0m  3477  prsspw  3796  disjnim  4025  brab1  4081  unopab  4113  exss  4261  uniuni  4487  elvvv  4727  eliunxp  4806  ralxp  4810  rexxp  4811  opelco  4839  reldm0  4885  resieq  4957  resiexg  4992  iss  4993  imai  5026  cnvsym  5054  intasym  5055  asymref  5056  codir  5059  poirr2  5063  rninxp  5114  cnvsom  5214  funopg  5293  fin  5447  f1cnvcnv  5477  fndmin  5672  resoprab  6022  mpo2eqb  6036  ov6g  6065  offval  6147  dfopab2  6256  dfoprab3s  6257  fmpox  6267  spc2ed  6300  brtpos0  6319  dftpos3  6329  tpostpos  6331  ercnv  6622  xpcomco  6894  xpassen  6898  phpm  6935  ctssdccl  7186  elni2  7398  elfz2nn0  10204  elfzmlbp  10224  clim0  11467  nnwosdc  12231  isstructim  12717  xpscf  13049  srgrmhm  13626  ntreq0  14452  cnmptcom  14618  dedekindicclemicc  14952