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  1861  2sb5  2002  2sb6  2003  2sb5rf  2008  2sb6rf  2009  moabs  2094  moanim  2119  2eu4  2138  2eu7  2139  sb8ab  2318  risset  2525  cbvreuvw  2735  reuind  2969  difundi  3416  indifdir  3420  unab  3431  inab  3432  rabeq0  3481  abeq0  3482  inssdif0im  3519  snprc  3688  snssOLD  3749  unipr  3854  uni0b  3865  pwtr  4253  opm  4268  onintexmid  4610  elxp2  4682  opthprc  4715  xpiundir  4723  elvvv  4727  relun  4781  inopab  4799  difopab  4800  ralxpf  4813  rexxpf  4814  dmiun  4876  rniun  5081  cnvresima  5160  imaco  5176  fnopabg  5384  dff1o2  5512  idref  5806  imaiun  5810  opabex3d  6187  opabex3  6188  onntri35  7320  elixx3g  9993  elfz2  10107  elfzuzb  10111  divalgb  12107  1nprm  12307  issubg3  13398  cnfldui  14221  alsconv  15811