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  1302  sbal1yz  1977  2exsb  1985  moanim  2074  2eu4  2093  cvjust  2135  abbi  2254  sbc8g  2920  ss2rab  3178  unass  3238  unss  3255  undi  3329  difindiss  3335  notm0  3388  disj  3416  unopab  4015  eqvinop  4173  pwexb  4403  dmun  4754  reldm0  4765  dmres  4848  imadmrn  4899  ssrnres  4989  dmsnm  5012  coundi  5048  coundir  5049  cnvpom  5089  xpcom  5093  fun11  5198  fununi  5199  funcnvuni  5200  isarep1  5217  fsn  5600  fconstfvm  5646  eufnfv  5656  acexmidlem2  5779  eloprabga  5866  funoprabg  5878  ralrnmpo  5893  rexrnmpo  5894  oprabrexex2  6036  dfer2  6438  euen1b  6705  xpsnen  6723  rexuz3  10794  tgval2  12259  ssntr  12330  metrest  12714  sinhalfpilem  12920