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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrri  207  3bitr3i  210  3bitr3ri  211  anandi  598  anandir  599  xchnxbi  691  orordi  785  orordir  786  sbco3v  2029  sbco4  2067  elsb1  2216  elsb2  2217  abeq1i  2350  cbvabw  2363  r19.41  2706  rexcom4a  2846  moeq  3001  mosubt  3003  2reuswapdc  3030  nfcdeq  3048  sbcid  3067  sbcco2  3074  sbc7  3078  sbcie2g  3085  eqsbc1  3091  sbcralt  3128  sbcrext  3129  cbvralcsf  3210  cbvrexcsf  3211  cbvrabcsf  3213  abss  3317  ssab  3318  difrab  3507  abn0m  3547  prsspw  3890  disjnim  4120  brab1  4178  unopab  4210  exss  4367  uniuni  4597  elvvv  4838  eliunxp  4919  ralxp  4923  rexxp  4924  opelco  4952  reldm0  4999  resieq  5073  resiexg  5108  iss  5109  imai  5143  cnvsym  5171  intasym  5172  asymref  5173  codir  5176  poirr2  5180  rninxp  5231  cnvsom  5331  funopg  5411  fin  5578  f1cnvcnv  5609  fndmin  5816  resoprab  6184  mpo2eqb  6198  ov6g  6227  offval  6310  dfopab2  6423  dfoprab3s  6424  fmpox  6436  spc2ed  6469  brtpos0  6523  dftpos3  6533  tpostpos  6535  ercnv  6828  xpcomco  7124  xpassen  7128  phpm  7167  ctssdccl  7451  elni2  7681  addeq0  8703  elfz2nn0  10519  elfzmlbp  10539  clim0  12051  nnwosdc  12816  ballotfilem7  13279  isstructim  13366  xpscf  13668  srgrmhm  14298  ntreq0  15233  cnmptcom  15399  dedekindicclemicc  15733