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  2025  sbco4  2063  elsb1  2212  elsb2  2213  abeq1i  2346  cbvabw  2359  r19.41  2700  rexcom4a  2840  moeq  2995  mosubt  2997  2reuswapdc  3024  nfcdeq  3042  sbcid  3061  sbcco2  3068  sbc7  3072  sbcie2g  3079  eqsbc1  3085  sbcralt  3122  sbcrext  3123  cbvralcsf  3204  cbvrexcsf  3205  cbvrabcsf  3207  abss  3311  ssab  3312  difrab  3499  abn0m  3538  prsspw  3874  disjnim  4104  brab1  4162  unopab  4194  exss  4348  uniuni  4577  elvvv  4818  eliunxp  4899  ralxp  4903  rexxp  4904  opelco  4932  reldm0  4979  resieq  5053  resiexg  5088  iss  5089  imai  5123  cnvsym  5151  intasym  5152  asymref  5153  codir  5156  poirr2  5160  rninxp  5211  cnvsom  5311  funopg  5391  fin  5558  f1cnvcnv  5589  fndmin  5790  resoprab  6157  mpo2eqb  6171  ov6g  6200  offval  6283  dfopab2  6396  dfoprab3s  6397  fmpox  6409  spc2ed  6442  brtpos0  6496  dftpos3  6506  tpostpos  6508  ercnv  6801  xpcomco  7090  xpassen  7094  phpm  7133  ctssdccl  7415  elni2  7645  addeq0  8666  elfz2nn0  10468  elfzmlbp  10488  clim0  11995  nnwosdc  12760  ballotfilem7  13223  isstructim  13310  xpscf  13611  srgrmhm  14237  ntreq0  15123  cnmptcom  15289  dedekindicclemicc  15623