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  682  pm4.15  684  3or6  1313  sbal1yz  1989  2exsb  1997  moanim  2088  2eu4  2107  cvjust  2160  abbi  2280  sbc8g  2958  ss2rab  3218  unass  3279  unss  3296  undi  3370  difindiss  3376  notm0  3429  disj  3457  unopab  4061  eqvinop  4221  pwexb  4452  dmun  4811  reldm0  4822  dmres  4905  imadmrn  4956  ssrnres  5046  dmsnm  5069  coundi  5105  coundir  5106  cnvpom  5146  xpcom  5150  fun11  5255  fununi  5256  funcnvuni  5257  isarep1  5274  fsn  5657  fconstfvm  5703  eufnfv  5715  acexmidlem2  5839  eloprabga  5929  funoprabg  5941  ralrnmpo  5956  rexrnmpo  5957  oprabrexex2  6098  dfer2  6502  euen1b  6769  xpsnen  6787  rexuz3  10932  tgval2  12691  ssntr  12762  metrest  13146  sinhalfpilem  13352