Theorem 3bitr4ri 213

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

Ref	Expression
3bitr4i.1	|- ( ph <-> ps )
3bitr4i.2	|- ( ch <-> ph )
3bitr4i.3	|- ( th <-> ps )

Assertion

Ref	Expression
3bitr4ri	|- ( th <-> ch )

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 |- ( ch <-> ph )
2		3bitr4i.1	. . 3 |- ( ph <-> ps )
3		3bitr4i.3	. . 3 |- ( th <-> ps )
4	2, 3	bitr4i 187	. 2 |- ( ph <-> th )
5	1, 4	bitr2i 185	1 |- ( th <-> ch )

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:  dcnnOLD  850  excxor  1389  sbequ8  1858  2sb5  1999  2sb6  2000  2sb5rf  2005  2sb6rf  2006  moabs  2091  moanim  2116  2eu4  2135  2eu7  2136  sb8ab  2315  risset  2522  cbvreuvw  2732  reuind  2965  difundi  3411  indifdir  3415  unab  3426  inab  3427  rabeq0  3476  abeq0  3477  inssdif0im  3514  snprc  3683  snssOLD  3744  unipr  3849  uni0b  3860  pwtr  4248  opm  4263  onintexmid  4605  elxp2  4677  opthprc  4710  xpiundir  4718  elvvv  4722  relun  4776  inopab  4794  difopab  4795  ralxpf  4808  rexxpf  4809  dmiun  4871  rniun  5076  cnvresima  5155  imaco  5171  fnopabg  5377  dff1o2  5505  idref  5799  imaiun  5803  opabex3d  6173  opabex3  6174  onntri35  7297  elixx3g  9967  elfz2  10081  elfzuzb  10085  divalgb  12066  1nprm  12252  issubg3  13262  cnfldui  14077  alsconv  15570