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  1996  sbco4  2034  elsb1  2182  elsb2  2183  abeq1i  2316  cbvabw  2327  r19.41  2660  rexcom4a  2795  moeq  2947  mosubt  2949  2reuswapdc  2976  nfcdeq  2994  sbcid  3013  sbcco2  3020  sbc7  3024  sbcie2g  3031  eqsbc1  3037  sbcralt  3074  sbcrext  3075  cbvralcsf  3155  cbvrexcsf  3156  cbvrabcsf  3158  abss  3261  ssab  3262  difrab  3446  abn0m  3485  prsspw  3805  disjnim  4034  brab1  4090  unopab  4122  exss  4270  uniuni  4496  elvvv  4736  eliunxp  4815  ralxp  4819  rexxp  4820  opelco  4848  reldm0  4894  resieq  4966  resiexg  5001  iss  5002  imai  5035  cnvsym  5063  intasym  5064  asymref  5065  codir  5068  poirr2  5072  rninxp  5123  cnvsom  5223  funopg  5302  fin  5456  f1cnvcnv  5486  fndmin  5681  resoprab  6031  mpo2eqb  6045  ov6g  6074  offval  6156  dfopab2  6265  dfoprab3s  6266  fmpox  6276  spc2ed  6309  brtpos0  6328  dftpos3  6338  tpostpos  6340  ercnv  6631  xpcomco  6903  xpassen  6907  phpm  6944  ctssdccl  7195  elni2  7409  elfz2nn0  10216  elfzmlbp  10236  clim0  11515  nnwosdc  12279  isstructim  12765  xpscf  13097  srgrmhm  13674  ntreq0  14522  cnmptcom  14688  dedekindicclemicc  15022