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  889  nanbi  1350  nic-ax  1490  2sb5  2171  2sb6  2172  2sb5rf  2181  2sb5rfOLD  2183  2sb6rfOLD  2184  moabs  2310  2mo2  2381  2eu7  2395  2eu8  2396  r3al  2844  r2exlem  2982  risset  2987  r19.35  3008  ralxpxfr2d  3228  reuind  3307  undif3  3759  unab  3765  inab  3766  inssdif0  3894  ssundif  3910  snss  4151  raldifsnb  4158  pwtp  4242  unipr  4258  uni0b  4270  iinuni  4409  reusv2lem4  4651  pwtr  4700  elxp2  5017  opthprc  5047  xpiundir  5055  elvvv  5059  xpsspwOLD  5117  relun  5119  inopab  5133  difopab  5134  ralxpf  5149  dmiun  5211  rniun  5416  cnvresima  5496  imaco  5512  fnopabg  5704  dff1o2  5821  brprcneu  5859  fnsuppresOLD  6121  idref  6141  imaiun  6145  sorpss  6569  opabex3d  6762  opabex3  6763  ovmptss  6864  fnsuppres  6927  rankc1  8288  aceq1  8498  dfac10  8517  fin41  8824  axgroth6  9206  genpass  9387  infm3  10502  prime  10941  elixx3g  11542  elfz2  11679  elfzuzb  11682  rpnnen2  13820  divalgb  13921  1nprm  14081  maxprmfct  14113  vdwmc  14355  imasleval  14796  issubm  15797  issubg3  16024  efgrelexlemb  16574  ist1-2  19642  elflim2  20228  isfcls  20273  istlm  20450  isnlm  20947  ishl2  21573  0wlk  24251  0trl  24252  erclwwlkref  24517  erclwwlknref  24529  h1de2ctlem  26177  nonbooli  26273  5oalem7  26282  ho01i  26451  rnbra  26730  cvnbtwn3  26911  chrelat2i  26988  moel  27086  disjex  27152  mptfnf  27199  maprnin  27254  ordtconlem1  27570  eulerpartgbij  27979  eulerpartlemr  27981  eulerpartlemn  27988  ballotlem2  28095  iscvm  28372  untuni  28584  dfso3  28600  dffr5  28787  nofulllem5  29071  brtxpsd3  29151  brbigcup  29153  fixcnv  29163  ellimits  29165  elfuns  29170  brimage  29181  brcart  29187  brimg  29192  brapply  29193  brcup  29194  brcap  29195  dfrdg4  29205  dfint3  29207  ellines  29407  mblfinlem2  29657  elicc3  29740  iscrngo2  30026  prtlem70  30224  prtlem100  30228  n0el  30232  prtlem15  30248  prter2  30254  inisegn0  30621  aaitgo  30744  isdomn3  30797  2sbc6g  30928  2sbc5g  30929  2reu7  31691  2reu8  31692  alsconv  32304  bnj976  32933  bnj1185  32949  bnj543  33048  bnj571  33061  bnj611  33073  bnj916  33088  bnj1000  33096  bnj1040  33125  bj-snsetex  33620  bj-snglc  33626  bj-projun  33651  lcvnbtwn3  33843  ishlat1  34167  ishlat2  34168  hlrelat2  34217  islpln5  34349  islvol5  34393  pclclN  34705  cdleme0nex  35104