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  886  nanbi  1340  nic-ax  1480  2sb5  2149  2sb6  2150  2sb5rf  2159  2sb5rfOLD  2161  2sb6rfOLD  2162  moabs  2288  2mo2  2359  2eu7  2373  2eu8  2374  risset  2768  r19.35  2872  ralxpxfr2d  3089  reuind  3167  undif3  3616  unab  3622  inab  3623  inssdif0  3751  ssundif  3767  snss  4004  pwtp  4093  unipr  4109  uni0b  4121  iinuni  4259  reusv2lem4  4501  pwtr  4550  elxp2  4863  opthprc  4891  xpiundir  4899  elvvv  4903  xpsspwOLD  4959  relun  4961  inopab  4975  difopab  4976  ralxpf  4991  dmiun  5053  rniun  5252  cnvresima  5332  imaco  5348  fnopabg  5539  dff1o2  5651  brprcneu  5689  fnsuppresOLD  5943  idref  5963  imaiun  5967  sorpss  6370  opabex3d  6560  opabex3  6561  ovmptss  6659  fnsuppres  6721  rankc1  8082  aceq1  8292  dfac10  8311  fin41  8618  axgroth6  9000  genpass  9183  infm3  10294  prime  10727  elixx3g  11318  elfz2  11449  elfzuzb  11452  rpnnen2  13513  divalgb  13613  1nprm  13773  maxprmfct  13804  vdwmc  14044  imasleval  14484  issubm  15480  issubg3  15704  efgrelexlemb  16252  ist1-2  18956  elflim2  19542  isfcls  19587  istlm  19764  isnlm  20261  ishl2  20887  0wlk  23449  0trl  23450  h1de2ctlem  24963  nonbooli  25059  5oalem7  25068  ho01i  25237  rnbra  25516  cvnbtwn3  25697  chrelat2i  25774  moel  25872  disjex  25939  mptfnf  25981  maprnin  26036  ordtconlem1  26359  eulerpartgbij  26760  eulerpartlemr  26762  eulerpartlemn  26769  ballotlem2  26876  iscvm  27153  untuni  27365  dfso3  27381  dffr5  27568  nofulllem5  27852  brtxpsd3  27932  brbigcup  27934  fixcnv  27944  ellimits  27946  elfuns  27951  brimage  27962  brcart  27968  brimg  27973  brapply  27974  brcup  27975  brcap  27976  dfrdg4  27986  dfint3  27988  ellines  28188  mblfinlem2  28434  elicc3  28517  iscrngo2  28803  prtlem70  29001  prtlem100  29005  n0el  29009  prtlem15  29025  prter2  29031  inisegn0  29401  aaitgo  29524  isdomn3  29577  2sbc6g  29674  2sbc5g  29675  2reu7  30020  2reu8  30021  raldifsnb  30128  erclwwlkref  30488  erclwwlknref  30504  alsconv  31147  bnj976  31776  bnj1185  31792  bnj543  31891  bnj571  31904  bnj611  31916  bnj916  31931  bnj1000  31939  bnj1040  31968  bj-snsetex  32461  bj-snglc  32467  bj-projun  32492  lcvnbtwn3  32678  ishlat1  33002  ishlat2  33003  hlrelat2  33052  islpln5  33184  islvol5  33228  pclclN  33540  cdleme0nex  33939