Theorem 3bitr4ri 269

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 243	. 2 |- (ph <-> th)
5	1, 4	bitr2i 241	1 |- (th <-> ch)

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  pm4.78  565  xor  861  nanbi  1294  nic-ax  1438  2sb5  2112  2sb6  2113  2sb5rf  2117  2sb6rf  2118  moabs  2248  2eu7  2290  2eu8  2291  risset  2661  r19.35  2758  reuind  3039  undif3  3515  unab  3521  inab  3522  inssdif0  3617  ssundif  3633  snss  3838  pwtp  3884  uni0b  3916  iinuni  4049  ssofss  4076  df1c2  4168  elxpk2  4197  dfuni12  4291  insklem  4304  dfuni3  4315  addcass  4415  ncfinraise  4481  ncfinlower  4483  nnadjoinlem1  4519  nnpweq  4523  sfin112  4529  dfop2lem1  4573  dfproj12  4576  setconslem2  4732  setconslem3  4733  setconslem7  4737  dfswap2  4741  elxp2  4802  xpiundir  4818  ralxpf  4827  brswap2  4860  inopab  4862  dfrn4  4904  dmeq0  4922  brres  4949  dfima3  4951  dmres  4986  rnuni  5038  dmsnn0  5064  cnvresima  5077  imaco  5086  dfcnv2  5100  fnopabg  5205  f1ocnvb  5298  imaiun  5464  isocnv2  5492  dfdm4  5507  dfrn5  5508  brimage  5793  otsnelsi3  5805  composeex  5820  disjex  5823  fnsex  5832  fnpprod  5843  crossex  5850  clos1baseima  5883  ecdmn0  5967  xpassen  6057  mucnc  6131  df0c2  6137  tcdi  6164  ce0nnul  6177  tc11  6228  finnc  6243  csucex  6259  nncdiv3lem1  6275