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-1 5  ax-2 6  ax-mp 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  664  pm4.15  830  3or6  1266  sbal1yz  1932  2exsb  1940  moanim  2029  2eu4  2048  cvjust  2090  abbi  2208  sbc8g  2861  ss2rab  3112  unass  3172  unss  3189  undi  3263  difindiss  3269  notm0  3322  disj  3350  unopab  3939  eqvinop  4094  pwexb  4324  dmun  4674  reldm0  4685  dmres  4766  imadmrn  4817  ssrnres  4907  dmsnm  4930  coundi  4966  coundir  4967  cnvpom  5007  xpcom  5011  fun11  5115  fununi  5116  funcnvuni  5117  isarep1  5134  fsn  5508  fconstfvm  5554  eufnfv  5564  acexmidlem2  5687  eloprabga  5773  funoprabg  5782  ralrnmpt2  5797  rexrnmpt2  5798  oprabrexex2  5939  dfer2  6333  euen1b  6600  xpsnen  6617  rexuz3  10538  tgval2  11903  ssntr  11974  metrest  12292