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  1996  sbco4  2034  elsb1  2182  elsb2  2183  abeq1i  2316  cbvabw  2327  r19.41  2660  rexcom4a  2795  moeq  2947  mosubt  2949  2reuswapdc  2976  nfcdeq  2994  sbcid  3013  sbcco2  3020  sbc7  3024  sbcie2g  3031  eqsbc1  3037  sbcralt  3074  sbcrext  3075  cbvralcsf  3155  cbvrexcsf  3156  cbvrabcsf  3158  abss  3261  ssab  3262  difrab  3446  abn0m  3485  prsspw  3805  disjnim  4034  brab1  4090  unopab  4122  exss  4270  uniuni  4497  elvvv  4737  eliunxp  4816  ralxp  4820  rexxp  4821  opelco  4849  reldm0  4895  resieq  4968  resiexg  5003  iss  5004  imai  5037  cnvsym  5065  intasym  5066  asymref  5067  codir  5070  poirr2  5074  rninxp  5125  cnvsom  5225  funopg  5304  fin  5461  f1cnvcnv  5491  fndmin  5686  resoprab  6040  mpo2eqb  6054  ov6g  6083  offval  6165  dfopab2  6274  dfoprab3s  6275  fmpox  6285  spc2ed  6318  brtpos0  6337  dftpos3  6347  tpostpos  6349  ercnv  6640  xpcomco  6920  xpassen  6924  phpm  6961  ctssdccl  7212  elni2  7426  elfz2nn0  10233  elfzmlbp  10253  clim0  11538  nnwosdc  12302  isstructim  12788  xpscf  13121  srgrmhm  13698  ntreq0  14546  cnmptcom  14712  dedekindicclemicc  15046