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  696  pm4.15  699  3or6  1357  sbal1yz  2052  2exsb  2060  moanim  2152  2eu4  2171  cvjust  2224  abbi  2343  sbc8g  3037  ss2rab  3301  unass  3362  unss  3379  undi  3453  difindiss  3459  notm0  3513  disj  3541  unopab  4166  eqvinop  4333  pwexb  4569  dmun  4936  reldm0  4947  dmres  5032  imadmrn  5084  ssrnres  5177  dmsnm  5200  coundi  5236  coundir  5237  cnvpom  5277  xpcom  5281  fun11  5394  fununi  5395  funcnvuni  5396  isarep1  5413  fsn  5815  fconstfvm  5867  eufnfv  5880  acexmidlem2  6010  eloprabga  6103  funoprabg  6115  ralrnmpo  6131  rexrnmpo  6132  oprabrexex2  6287  dfer2  6698  euen1b  6972  xpsnen  7000  rexuz3  11541  imasaddfnlemg  13387  subsubrng2  14219  subsubrg2  14250  tgval2  14765  ssntr  14836  metrest  15220  plyun0  15450  sinhalfpilem  15505  2lgslem4  15822  wlkeq  16151  clwwlkn1  16213  clwwlkn2  16216  clwwlknon2x  16230