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  856  excxor  1422  sbequ8  1895  2sb5  2036  2sb6  2037  2sb5rf  2042  2sb6rf  2043  moabs  2129  moanim  2154  2eu4  2173  2eu7  2174  sb8ab  2353  risset  2560  cbvreuvw  2773  reuind  3011  difundi  3459  indifdir  3463  unab  3474  inab  3475  rabeq0  3524  abeq0  3525  inssdif0im  3562  snprc  3734  snssOLD  3799  unipr  3907  uni0b  3918  pwtr  4311  opm  4326  onintexmid  4671  elxp2  4743  opthprc  4777  xpiundir  4785  elvvv  4789  relun  4844  inopab  4862  difopab  4863  ralxpf  4876  rexxpf  4877  dmiun  4940  rniun  5147  cnvresima  5226  imaco  5242  fnopabg  5456  dff1o2  5588  idref  5896  imaiun  5900  opabex3d  6282  opabex3  6283  onntri35  7454  elixx3g  10135  elfz2  10249  elfzuzb  10253  divalgb  12485  1nprm  12685  issubg3  13778  cnfldui  14602  alsconv  16691