Theorem 3bitr4ri 281

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

Syntax hints:   <-> wb 187

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 188

This theorem is referenced by:  pm4.78  584  xor  899  nannan  1384  nanbiOLDOLD  1390  nic-ax  1552  2sb5  2238  2sb6  2239  2sb5rf  2246  moabs  2297  2mo2  2346  2eu7  2357  2eu8  2358  r3al  2805  r2exlem  2948  risset  2953  r19.35  2975  ralxpxfr2d  3196  reuind  3275  undif3  3734  unab  3740  inab  3741  inssdif0  3862  ssundif  3879  snss  4121  raldifsnb  4128  pwtp  4213  unipr  4229  uni0b  4241  iinuni  4383  reusv2lem4  4624  pwtr  4670  elxp2  4867  opthprc  4897  xpiundir  4905  elvvv  4909  xpsspw  4963  relun  4965  inopab  4980  difopab  4981  ralxpf  4996  dmiun  5058  inisegn0  5215  rniun  5261  cnvresima  5339  imaco  5355  mptfnf  5713  fnopabg  5715  dff1o2  5832  brprcneu  5870  idref  6157  imaiun  6161  sorpss  6586  opabex3d  6781  opabex3  6782  ovmptss  6884  fnsuppres  6949  rankc1  8342  aceq1  8548  dfac10  8567  fin41  8874  axgroth6  9253  genpass  9434  infm3  10568  prime  11016  elixx3g  11648  elfz2  11791  elfzuzb  11794  rpnnen2  14263  divalgb  14370  1nprm  14614  maxprmfct  14637  vdwmc  14913  imasleval  15432  issubm  16579  issubg3  16820  efgrelexlemb  17385  ist1-2  20347  unisngl  20526  elflim2  20963  isfcls  21008  istlm  21183  isnlm  21662  ishl2  22321  0wlk  25258  0trl  25259  erclwwlkref  25524  erclwwlknref  25536  h1de2ctlem  27191  nonbooli  27287  5oalem7  27296  ho01i  27464  rnbra  27743  cvnbtwn3  27924  chrelat2i  28001  moel  28102  uniinn0  28150  disjex  28189  maprnin  28307  ordtconlem1  28723  esum2dlem  28906  eulerpartgbij  29198  eulerpartlemr  29200  eulerpartlemn  29207  ballotlem2  29314  bnj976  29582  bnj1185  29598  bnj543  29697  bnj571  29710  bnj611  29722  bnj916  29737  bnj1000  29745  bnj1040  29774  iscvm  29975  untuni  30329  dfso3  30345  dffr5  30385  nofulllem5  30585  brtxpsd3  30653  brbigcup  30655  fixcnv  30665  ellimits  30667  elfuns  30672  brimage  30683  brcart  30689  brimg  30694  brapply  30695  brcup  30696  brcap  30697  dfrdg4  30708  dfint3  30709  ellines  30909  elicc3  30963  bj-snsetex  31510  bj-snglc  31516  bj-projun  31541  wl-cases2-dnf  31761  poimirlem27  31878  mblfinlem2  31889  iscrngo2  32142  prtlem70  32338  prtlem100  32342  n0el  32346  prtlem15  32362  prter2  32368  lcvnbtwn3  32510  ishlat1  32834  ishlat2  32835  hlrelat2  32884  islpln5  33016  islvol5  33060  pclclN  33372  cdleme0nex  33772  aaitgo  35945  isdomn3  35998  imaiun1  36100  relexp0eq  36150  2sbc6g  36621  2sbc5g  36622  2reu7  38322  2reu8  38323  alsconv  39717