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  693  pm4.15  695  3or6  1334  sbal1yz  2017  2exsb  2025  moanim  2116  2eu4  2135  cvjust  2188  abbi  2307  sbc8g  2994  ss2rab  3256  unass  3317  unss  3334  undi  3408  difindiss  3414  notm0  3468  disj  3496  unopab  4109  eqvinop  4273  pwexb  4506  dmun  4870  reldm0  4881  dmres  4964  imadmrn  5016  ssrnres  5109  dmsnm  5132  coundi  5168  coundir  5169  cnvpom  5209  xpcom  5213  fun11  5322  fununi  5323  funcnvuni  5324  isarep1  5341  fsn  5731  fconstfvm  5777  eufnfv  5790  acexmidlem2  5916  eloprabga  6006  funoprabg  6018  ralrnmpo  6034  rexrnmpo  6035  oprabrexex2  6184  dfer2  6590  euen1b  6859  xpsnen  6877  rexuz3  11137  imasaddfnlemg  12900  subsubrng2  13714  subsubrg2  13745  tgval2  14230  ssntr  14301  metrest  14685  plyun0  14915  sinhalfpilem  14967  2lgslem4  15260