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  680  orordi  773  orordir  774  sbco3v  1969  sbco4  2007  elsb1  2155  elsb2  2156  abeq1i  2289  cbvabw  2300  r19.41  2632  rexcom4a  2761  moeq  2912  mosubt  2914  2reuswapdc  2941  nfcdeq  2959  sbcid  2978  sbcco2  2985  sbc7  2989  sbcie2g  2996  eqsbc1  3002  sbcralt  3039  sbcrext  3040  cbvralcsf  3119  cbvrexcsf  3120  cbvrabcsf  3122  abss  3224  ssab  3225  difrab  3409  abn0m  3448  prsspw  3765  disjnim  3994  brab1  4050  unopab  4082  exss  4227  uniuni  4451  elvvv  4689  eliunxp  4766  ralxp  4770  rexxp  4771  opelco  4799  reldm0  4845  resieq  4917  resiexg  4952  iss  4953  imai  4984  cnvsym  5012  intasym  5013  asymref  5014  codir  5017  poirr2  5021  rninxp  5072  cnvsom  5172  funopg  5250  fin  5402  f1cnvcnv  5432  fndmin  5623  resoprab  5970  mpo2eqb  5983  ov6g  6011  offval  6089  dfopab2  6189  dfoprab3s  6190  fmpox  6200  spc2ed  6233  brtpos0  6252  dftpos3  6262  tpostpos  6264  ercnv  6555  xpcomco  6825  xpassen  6829  phpm  6864  ctssdccl  7109  elni2  7312  elfz2nn0  10111  elfzmlbp  10131  clim0  11292  nnwosdc  12039  isstructim  12475  xpscf  12765  srgrmhm  13175  ntreq0  13602  cnmptcom  13768  dedekindicclemicc  14080