Theorem bitr2i 184

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr2i.1	|- ( ph <-> ps )
bitr2i.2	|- ( ps <-> ch )

Assertion

Ref	Expression
bitr2i	|- ( ch <-> ph )

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 |- ( ph <-> ps )
2		bitr2i.2	. . 3 |- ( ps <-> ch )
3	1, 2	bitri 183	. 2 |- ( ph <-> ch )
4	3	bicomi 131	1 |- ( ch <-> ph )

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  3bitr2ri  208  3bitr4ri  212  nan  681  pm4.15  683  3or6  1301  sbal1yz  1976  2exsb  1984  moanim  2073  2eu4  2092  cvjust  2134  abbi  2253  sbc8g  2916  ss2rab  3173  unass  3233  unss  3250  undi  3324  difindiss  3330  notm0  3383  disj  3411  unopab  4007  eqvinop  4165  pwexb  4395  dmun  4746  reldm0  4757  dmres  4840  imadmrn  4891  ssrnres  4981  dmsnm  5004  coundi  5040  coundir  5041  cnvpom  5081  xpcom  5085  fun11  5190  fununi  5191  funcnvuni  5192  isarep1  5209  fsn  5592  fconstfvm  5638  eufnfv  5648  acexmidlem2  5771  eloprabga  5858  funoprabg  5870  ralrnmpo  5885  rexrnmpo  5886  oprabrexex2  6028  dfer2  6430  euen1b  6697  xpsnen  6715  rexuz3  10762  tgval2  12220  ssntr  12291  metrest  12675  sinhalfpilem  12872