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  2662  r19.35  2759  reuind  3040  undif3  3516  unab  3522  inab  3523  inssdif0  3618  ssundif  3634  snss  3839  pwtp  3885  uni0b  3917  iinuni  4050  ssofss  4077  df1c2  4169  elxpk2  4198  dfuni12  4292  insklem  4305  dfuni3  4316  addcass  4416  ncfinraise  4482  ncfinlower  4484  nnadjoinlem1  4520  nnpweq  4524  sfin112  4530  dfop2lem1  4574  dfproj12  4577  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  elxp2  4803  xpiundir  4819  ralxpf  4828  brswap2  4861  inopab  4863  dfrn4  4905  dmeq0  4923  brres  4950  dfima3  4952  dmres  4987  rnuni  5039  dmsnn0  5065  cnvresima  5078  imaco  5087  dfcnv2  5101  fnopabg  5206  f1ocnvb  5299  imaiun  5465  isocnv2  5493  dfdm4  5508  dfrn5  5509  brimage  5794  otsnelsi3  5806  composeex  5821  disjex  5824  fnsex  5833  fnpprod  5844  crossex  5851  clos1baseima  5884  ecdmn0  5968  xpassen  6058  mucnc  6132  df0c2  6138  tcdi  6165  ce0nnul  6178  tc11  6229  finnc  6244  csucex  6260  nncdiv3lem1  6276