Theorem 3bitr4ri 280

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

Syntax hints:   <-> wb 186

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 187

This theorem is referenced by:  pm4.78  582  xor  894  nannan  1352  nanbiOLDOLD  1358  nic-ax  1528  2sb5  2213  2sb6  2214  2sb5rf  2221  moabs  2273  2mo2  2325  2eu7  2338  2eu8  2339  r3al  2786  r2exlem  2929  risset  2934  r19.35  2956  ralxpxfr2d  3176  reuind  3255  undif3  3713  unab  3719  inab  3720  inssdif0  3841  ssundif  3857  snss  4098  raldifsnb  4105  pwtp  4190  unipr  4206  uni0b  4218  iinuni  4360  reusv2lem4  4600  pwtr  4646  elxp2  4843  opthprc  4873  xpiundir  4881  elvvv  4885  xpsspw  4939  relun  4941  inopab  4956  difopab  4957  ralxpf  4972  dmiun  5034  rniun  5236  cnvresima  5314  imaco  5330  mptfnf  5687  fnopabg  5689  dff1o2  5806  brprcneu  5844  fnsuppresOLD  6115  idref  6136  imaiun  6140  sorpss  6569  opabex3d  6764  opabex3  6765  ovmptss  6867  fnsuppres  6932  rankc1  8322  aceq1  8532  dfac10  8551  fin41  8858  axgroth6  9238  genpass  9419  infm3  10544  prime  10986  elixx3g  11597  elfz2  11735  elfzuzb  11738  rpnnen2  14170  divalgb  14273  1nprm  14433  maxprmfct  14465  vdwmc  14707  imasleval  15157  issubm  16304  issubg3  16545  efgrelexlemb  17094  ist1-2  20143  unisngl  20322  elflim2  20759  isfcls  20804  istlm  20981  isnlm  21478  ishl2  22104  0wlk  24976  0trl  24977  erclwwlkref  25242  erclwwlknref  25254  h1de2ctlem  26900  nonbooli  26996  5oalem7  27005  ho01i  27173  rnbra  27452  cvnbtwn3  27633  chrelat2i  27710  moel  27810  uniinn0  27858  disjex  27897  maprnin  28014  ordtconlem1  28372  esum2dlem  28552  eulerpartgbij  28830  eulerpartlemr  28832  eulerpartlemn  28839  ballotlem2  28946  bnj976  29176  bnj1185  29192  bnj543  29291  bnj571  29304  bnj611  29316  bnj916  29331  bnj1000  29339  bnj1040  29368  iscvm  29569  untuni  29923  dfso3  29939  dffr5  29979  nofulllem5  30179  brtxpsd3  30247  brbigcup  30249  fixcnv  30259  ellimits  30261  elfuns  30266  brimage  30277  brcart  30283  brimg  30288  brapply  30289  brcup  30290  brcap  30291  dfrdg4  30302  dfint3  30303  ellines  30503  elicc3  30558  bj-snsetex  31099  bj-snglc  31105  bj-projun  31130  wl-cases2-dnf  31350  mblfinlem2  31437  iscrngo2  31690  prtlem70  31887  prtlem100  31891  n0el  31895  prtlem15  31911  prter2  31917  lcvnbtwn3  32059  ishlat1  32383  ishlat2  32384  hlrelat2  32433  islpln5  32565  islvol5  32609  pclclN  32921  cdleme0nex  33321  inisegn0  35364  aaitgo  35488  isdomn3  35541  imaiun1  35643  relexp0eq  35693  2sbc6g  36183  2sbc5g  36184  2reu7  37577  2reu8  37578  alsconv  38862