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  1985  sbco4  2023  elsb1  2171  elsb2  2172  abeq1i  2305  cbvabw  2316  r19.41  2649  rexcom4a  2784  moeq  2935  mosubt  2937  2reuswapdc  2964  nfcdeq  2982  sbcid  3001  sbcco2  3008  sbc7  3012  sbcie2g  3019  eqsbc1  3025  sbcralt  3062  sbcrext  3063  cbvralcsf  3143  cbvrexcsf  3144  cbvrabcsf  3146  abss  3248  ssab  3249  difrab  3433  abn0m  3472  prsspw  3791  disjnim  4020  brab1  4076  unopab  4108  exss  4256  uniuni  4482  elvvv  4722  eliunxp  4801  ralxp  4805  rexxp  4806  opelco  4834  reldm0  4880  resieq  4952  resiexg  4987  iss  4988  imai  5021  cnvsym  5049  intasym  5050  asymref  5051  codir  5054  poirr2  5058  rninxp  5109  cnvsom  5209  funopg  5288  fin  5440  f1cnvcnv  5470  fndmin  5665  resoprab  6014  mpo2eqb  6028  ov6g  6056  offval  6138  dfopab2  6242  dfoprab3s  6243  fmpox  6253  spc2ed  6286  brtpos0  6305  dftpos3  6315  tpostpos  6317  ercnv  6608  xpcomco  6880  xpassen  6884  phpm  6921  ctssdccl  7170  elni2  7374  elfz2nn0  10178  elfzmlbp  10198  clim0  11428  nnwosdc  12176  isstructim  12632  xpscf  12930  srgrmhm  13490  ntreq0  14300  cnmptcom  14466  dedekindicclemicc  14786