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  2023  sbco4  2061  elsb1  2210  elsb2  2211  abeq1i  2344  cbvabw  2357  r19.41  2698  rexcom4a  2838  moeq  2992  mosubt  2994  2reuswapdc  3021  nfcdeq  3039  sbcid  3058  sbcco2  3065  sbc7  3069  sbcie2g  3076  eqsbc1  3082  sbcralt  3119  sbcrext  3120  cbvralcsf  3201  cbvrexcsf  3202  cbvrabcsf  3204  abss  3307  ssab  3308  difrab  3495  abn0m  3534  prsspw  3869  disjnim  4099  brab1  4157  unopab  4189  exss  4343  uniuni  4572  elvvv  4813  eliunxp  4894  ralxp  4898  rexxp  4899  opelco  4927  reldm0  4974  resieq  5048  resiexg  5083  iss  5084  imai  5118  cnvsym  5146  intasym  5147  asymref  5148  codir  5151  poirr2  5155  rninxp  5206  cnvsom  5306  funopg  5386  fin  5553  f1cnvcnv  5584  fndmin  5785  resoprab  6149  mpo2eqb  6163  ov6g  6192  offval  6274  dfopab2  6383  dfoprab3s  6384  fmpox  6396  spc2ed  6429  brtpos0  6483  dftpos3  6493  tpostpos  6495  ercnv  6788  xpcomco  7077  xpassen  7081  phpm  7120  ctssdccl  7402  elni2  7629  elfz2nn0  10446  elfzmlbp  10466  clim0  11970  nnwosdc  12735  isstructim  13226  xpscf  13560  srgrmhm  14138  ntreq0  14997  cnmptcom  15163  dedekindicclemicc  15497