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  687  pm4.15  689  3or6  1318  sbal1yz  1994  2exsb  2002  moanim  2093  2eu4  2112  cvjust  2165  abbi  2284  sbc8g  2962  ss2rab  3223  unass  3284  unss  3301  undi  3375  difindiss  3381  notm0  3435  disj  3463  unopab  4068  eqvinop  4228  pwexb  4459  dmun  4818  reldm0  4829  dmres  4912  imadmrn  4963  ssrnres  5053  dmsnm  5076  coundi  5112  coundir  5113  cnvpom  5153  xpcom  5157  fun11  5265  fununi  5266  funcnvuni  5267  isarep1  5284  fsn  5668  fconstfvm  5714  eufnfv  5726  acexmidlem2  5850  eloprabga  5940  funoprabg  5952  ralrnmpo  5967  rexrnmpo  5968  oprabrexex2  6109  dfer2  6514  euen1b  6781  xpsnen  6799  rexuz3  10954  tgval2  12845  ssntr  12916  metrest  13300  sinhalfpilem  13506