Theorem bitr2i 185

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 184	. 2 |- ( ph <-> ch )
4	3	bicomi 132	1 |- ( ch <-> ph )

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrri  207  3bitr2ri  209  3bitr4ri  213  nan  692  pm4.15  694  3or6  1323  sbal1yz  2001  2exsb  2009  moanim  2100  2eu4  2119  cvjust  2172  abbi  2291  sbc8g  2970  ss2rab  3231  unass  3292  unss  3309  undi  3383  difindiss  3389  notm0  3443  disj  3471  unopab  4082  eqvinop  4243  pwexb  4474  dmun  4834  reldm0  4845  dmres  4928  imadmrn  4980  ssrnres  5071  dmsnm  5094  coundi  5130  coundir  5131  cnvpom  5171  xpcom  5175  fun11  5283  fununi  5284  funcnvuni  5285  isarep1  5302  fsn  5688  fconstfvm  5734  eufnfv  5747  acexmidlem2  5871  eloprabga  5961  funoprabg  5973  ralrnmpo  5988  rexrnmpo  5989  oprabrexex2  6130  dfer2  6535  euen1b  6802  xpsnen  6820  rexuz3  10998  imasaddfnlemg  12734  subsubrg2  13365  tgval2  13521  ssntr  13592  metrest  13976  sinhalfpilem  14182