Theorem 3bitr4ri 278

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

Syntax hints:   <-> wb 184

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 185

This theorem is referenced by:  pm4.78  582  xor  891  nannan  1349  nanbiOLD  1354  nic-ax  1493  2sb5  2173  2sb6  2174  2sb5rf  2181  moabs  2301  2mo2  2358  2eu7  2371  2eu8  2372  r3al  2823  r2exlem  2963  risset  2968  r19.35  2990  ralxpxfr2d  3210  reuind  3289  undif3  3744  unab  3750  inab  3751  inssdif0  3881  ssundif  3897  snss  4139  raldifsnb  4146  pwtp  4231  unipr  4247  uni0b  4259  iinuni  4399  reusv2lem4  4641  pwtr  4690  elxp2  5007  opthprc  5037  xpiundir  5045  elvvv  5049  xpsspwOLD  5107  relun  5109  inopab  5123  difopab  5124  ralxpf  5139  dmiun  5201  rniun  5406  cnvresima  5486  imaco  5502  fnopabg  5694  dff1o2  5811  brprcneu  5849  fnsuppresOLD  6116  idref  6138  imaiun  6142  sorpss  6570  opabex3d  6763  opabex3  6764  ovmptss  6866  fnsuppres  6929  rankc1  8291  aceq1  8501  dfac10  8520  fin41  8827  axgroth6  9209  genpass  9390  infm3  10509  prime  10950  elixx3g  11552  elfz2  11689  elfzuzb  11692  rpnnen2  13940  divalgb  14043  1nprm  14203  maxprmfct  14235  vdwmc  14477  imasleval  14919  issubm  15956  issubg3  16197  efgrelexlemb  16746  ist1-2  19825  unisngl  20005  elflim2  20442  isfcls  20487  istlm  20664  isnlm  21161  ishl2  21787  0wlk  24523  0trl  24524  erclwwlkref  24789  erclwwlknref  24801  h1de2ctlem  26449  nonbooli  26545  5oalem7  26554  ho01i  26723  rnbra  27002  cvnbtwn3  27183  chrelat2i  27260  moel  27358  uniinn0  27400  disjex  27427  mptfnf  27475  maprnin  27530  ordtconlem1  27883  eulerpartgbij  28288  eulerpartlemr  28290  eulerpartlemn  28297  ballotlem2  28404  iscvm  28681  untuni  29058  dfso3  29074  dffr5  29157  nofulllem5  29441  brtxpsd3  29521  brbigcup  29523  fixcnv  29533  ellimits  29535  elfuns  29540  brimage  29551  brcart  29557  brimg  29562  brapply  29563  brcup  29564  brcap  29565  dfrdg4  29575  dfint3  29577  ellines  29777  mblfinlem2  30027  elicc3  30110  iscrngo2  30370  prtlem70  30567  prtlem100  30571  n0el  30575  prtlem15  30591  prter2  30597  inisegn0  30964  aaitgo  31087  isdomn3  31140  2sbc6g  31276  2sbc5g  31277  2reu7  32034  2reu8  32035  alsconv  32940  bnj976  33569  bnj1185  33585  bnj543  33684  bnj571  33697  bnj611  33709  bnj916  33724  bnj1000  33732  bnj1040  33761  bj-snsetex  34269  bj-snglc  34275  bj-projun  34300  lcvnbtwn3  34493  ishlat1  34817  ishlat2  34818  hlrelat2  34867  islpln5  34999  islvol5  35043  pclclN  35355  cdleme0nex  35755