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  4162  eqvinop  4328  pwexb  4564  dmun  4929  reldm0  4940  dmres  5025  imadmrn  5077  ssrnres  5170  dmsnm  5193  coundi  5229  coundir  5230  cnvpom  5270  xpcom  5274  fun11  5387  fununi  5388  funcnvuni  5389  isarep1  5406  fsn  5806  fconstfvm  5856  eufnfv  5869  acexmidlem2  5997  eloprabga  6090  funoprabg  6102  ralrnmpo  6118  rexrnmpo  6119  oprabrexex2  6273  dfer2  6679  euen1b  6953  xpsnen  6976  rexuz3  11496  imasaddfnlemg  13342  subsubrng2  14173  subsubrg2  14204  tgval2  14719  ssntr  14790  metrest  15174  plyun0  15404  sinhalfpilem  15459  2lgslem4  15776