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  851  excxor  1398  sbequ8  1871  2sb5  2012  2sb6  2013  2sb5rf  2018  2sb6rf  2019  moabs  2105  moanim  2130  2eu4  2149  2eu7  2150  sb8ab  2329  risset  2536  cbvreuvw  2748  reuind  2985  difundi  3433  indifdir  3437  unab  3448  inab  3449  rabeq0  3498  abeq0  3499  inssdif0im  3536  snprc  3708  snssOLD  3770  unipr  3878  uni0b  3889  pwtr  4281  opm  4296  onintexmid  4639  elxp2  4711  opthprc  4744  xpiundir  4752  elvvv  4756  relun  4810  inopab  4828  difopab  4829  ralxpf  4842  rexxpf  4843  dmiun  4906  rniun  5112  cnvresima  5191  imaco  5207  fnopabg  5419  dff1o2  5549  idref  5848  imaiun  5852  opabex3d  6229  opabex3  6230  onntri35  7383  elixx3g  10058  elfz2  10172  elfzuzb  10176  divalgb  12351  1nprm  12551  issubg3  13643  cnfldui  14466  alsconv  16221