Theorem bitr3i 185

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 131	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 183	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrri  206  3bitr3i  209  3bitr3ri  210  anandi  585  anandir  586  xchnxbi  675  orordi  768  orordir  769  sbco3v  1962  sbco4  2000  elsb1  2148  elsb2  2149  abeq1i  2282  cbvabw  2293  r19.41  2625  rexcom4a  2754  moeq  2905  mosubt  2907  2reuswapdc  2934  nfcdeq  2952  sbcid  2970  sbcco2  2977  sbc7  2981  sbcie2g  2988  eqsbc1  2994  sbcralt  3031  sbcrext  3032  cbvralcsf  3111  cbvrexcsf  3112  cbvrabcsf  3114  abss  3216  ssab  3217  difrab  3401  abn0m  3440  prsspw  3752  disjnim  3980  brab1  4036  unopab  4068  exss  4212  uniuni  4436  elvvv  4674  eliunxp  4750  ralxp  4754  rexxp  4755  opelco  4783  reldm0  4829  resieq  4901  resiexg  4936  iss  4937  imai  4967  cnvsym  4994  intasym  4995  asymref  4996  codir  4999  poirr2  5003  rninxp  5054  cnvsom  5154  funopg  5232  fin  5384  f1cnvcnv  5414  fndmin  5603  resoprab  5949  mpo2eqb  5962  ov6g  5990  offval  6068  dfopab2  6168  dfoprab3s  6169  fmpox  6179  spc2ed  6212  brtpos0  6231  dftpos3  6241  tpostpos  6243  ercnv  6534  xpcomco  6804  xpassen  6808  phpm  6843  ctssdccl  7088  elni2  7276  elfz2nn0  10068  elfzmlbp  10088  clim0  11248  nnwosdc  11994  isstructim  12430  ntreq0  12926  cnmptcom  13092  dedekindicclemicc  13404