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  3036  ss2rab  3300  unass  3361  unss  3378  undi  3452  difindiss  3458  notm0  3512  disj  3540  unopab  4163  eqvinop  4329  pwexb  4565  dmun  4930  reldm0  4941  dmres  5026  imadmrn  5078  ssrnres  5171  dmsnm  5194  coundi  5230  coundir  5231  cnvpom  5271  xpcom  5275  fun11  5388  fununi  5389  funcnvuni  5390  isarep1  5407  fsn  5809  fconstfvm  5861  eufnfv  5874  acexmidlem2  6004  eloprabga  6097  funoprabg  6109  ralrnmpo  6125  rexrnmpo  6126  oprabrexex2  6281  dfer2  6689  euen1b  6963  xpsnen  6988  rexuz3  11516  imasaddfnlemg  13362  subsubrng2  14194  subsubrg2  14225  tgval2  14740  ssntr  14811  metrest  15195  plyun0  15425  sinhalfpilem  15480  2lgslem4  15797  wlkeq  16095