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  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  3885  disjnim  4115  brab1  4173  unopab  4205  exss  4362  uniuni  4592  elvvv  4833  eliunxp  4914  ralxp  4918  rexxp  4919  opelco  4947  reldm0  4994  resieq  5068  resiexg  5103  iss  5104  imai  5138  cnvsym  5166  intasym  5167  asymref  5168  codir  5171  poirr2  5175  rninxp  5226  cnvsom  5326  funopg  5406  fin  5573  f1cnvcnv  5604  fndmin  5807  resoprab  6174  mpo2eqb  6188  ov6g  6217  offval  6300  dfopab2  6413  dfoprab3s  6414  fmpox  6426  spc2ed  6459  brtpos0  6513  dftpos3  6523  tpostpos  6525  ercnv  6818  xpcomco  7114  xpassen  7118  phpm  7157  ctssdccl  7441  elni2  7671  addeq0  8693  elfz2nn0  10497  elfzmlbp  10517  clim0  12029  nnwosdc  12794  ballotfilem7  13257  isstructim  13344  xpscf  13645  srgrmhm  14272  ntreq0  15156  cnmptcom  15322  dedekindicclemicc  15656