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  4179  unopab  4211  exss  4369  uniuni  4599  elvvv  4840  eliunxp  4921  ralxp  4925  rexxp  4926  opelco  4954  reldm0  5001  resieq  5075  resiexg  5111  iss  5112  imai  5146  cnvsym  5174  intasym  5175  asymref  5176  codir  5179  poirr2  5183  rninxp  5234  cnvsom  5334  funopg  5414  fin  5581  f1cnvcnv  5612  fndmin  5819  resoprab  6187  mpo2eqb  6201  ov6g  6230  offval  6314  dfopab2  6427  dfoprab3s  6428  fmpox  6440  spc2ed  6473  brtpos0  6527  dftpos3  6537  tpostpos  6539  ercnv  6832  xpcomco  7128  xpassen  7132  phpm  7171  ctssdccl  7457  elni2  7687  addeq0  8710  elfz2nn0  10536  elfzmlbp  10556  clim0  12076  nnwosdc  12841  ballotfilem7  13337  isstructim  13424  xpscf  13727  srgrmhm  14405  ntreq0  15358  cnmptcom  15524  dedekindicclemicc  15858