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  854  excxor  1420  sbequ8  1893  2sb5  2034  2sb6  2035  2sb5rf  2040  2sb6rf  2041  moabs  2127  moanim  2152  2eu4  2171  2eu7  2172  sb8ab  2351  risset  2558  cbvreuvw  2771  reuind  3008  difundi  3456  indifdir  3460  unab  3471  inab  3472  rabeq0  3521  abeq0  3522  inssdif0im  3559  snprc  3731  snssOLD  3793  unipr  3901  uni0b  3912  pwtr  4304  opm  4319  onintexmid  4664  elxp2  4736  opthprc  4769  xpiundir  4777  elvvv  4781  relun  4835  inopab  4853  difopab  4854  ralxpf  4867  rexxpf  4868  dmiun  4931  rniun  5138  cnvresima  5217  imaco  5233  fnopabg  5446  dff1o2  5576  idref  5879  imaiun  5883  opabex3d  6264  opabex3  6265  onntri35  7418  elixx3g  10093  elfz2  10207  elfzuzb  10211  divalgb  12431  1nprm  12631  issubg3  13724  cnfldui  14547  alsconv  16407