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  687  orordi  781  orordir  782  sbco3v  2022  sbco4  2060  elsb1  2209  elsb2  2210  abeq1i  2343  cbvabw  2355  r19.41  2689  rexcom4a  2828  moeq  2982  mosubt  2984  2reuswapdc  3011  nfcdeq  3029  sbcid  3048  sbcco2  3055  sbc7  3059  sbcie2g  3066  eqsbc1  3072  sbcralt  3109  sbcrext  3110  cbvralcsf  3191  cbvrexcsf  3192  cbvrabcsf  3194  abss  3297  ssab  3298  difrab  3483  abn0m  3522  prsspw  3853  disjnim  4083  brab1  4141  unopab  4173  exss  4325  uniuni  4554  elvvv  4795  eliunxp  4875  ralxp  4879  rexxp  4880  opelco  4908  reldm0  4955  resieq  5029  resiexg  5064  iss  5065  imai  5099  cnvsym  5127  intasym  5128  asymref  5129  codir  5132  poirr2  5136  rninxp  5187  cnvsom  5287  funopg  5367  fin  5531  f1cnvcnv  5562  fndmin  5763  resoprab  6127  mpo2eqb  6141  ov6g  6170  offval  6252  dfopab2  6361  dfoprab3s  6362  fmpox  6374  spc2ed  6407  brtpos0  6461  dftpos3  6471  tpostpos  6473  ercnv  6766  xpcomco  7053  xpassen  7057  phpm  7095  ctssdccl  7353  elni2  7577  elfz2nn0  10392  elfzmlbp  10412  clim0  11908  nnwosdc  12673  isstructim  13159  xpscf  13493  srgrmhm  14071  ntreq0  14926  cnmptcom  15092  dedekindicclemicc  15426