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  861  excxor  1427  sbequ8  1900  2sb5  2043  2sb6  2044  2sb5rf  2049  2sb6rf  2050  moabs  2136  moanim  2161  2eu4  2180  2eu7  2181  sb8ab  2362  risset  2578  cbvreuvw  2792  reuind  3031  difundi  3483  indifdir  3487  unab  3498  inab  3499  rabeq0  3552  abeq0  3553  inssdif0im  3591  snprc  3770  snssOLD  3835  unipr  3944  uni0b  3955  pwtr  4354  opm  4369  onintexmid  4715  elxp2  4787  opthprc  4821  xpiundir  4829  elvvv  4833  relun  4889  inopab  4907  difopab  4908  ralxpf  4921  rexxpf  4922  dmiun  4985  rniun  5193  cnvresima  5272  imaco  5288  fnopabg  5502  dff1o2  5639  idref  5952  imaiun  5956  opabex3d  6340  opabex3  6341  onntri35  7586  elixx3g  10282  elfz2  10397  elfzuzb  10401  divalgb  12670  1nprm  12870  issubg3  13972  cnfldui  14896  alsconv  17035