Theorem 3bitr4ri 286

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

Syntax hints:   <-> wb 189

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 190

This theorem is referenced by:  pm4.78  592  xor  908  nannan  1416  nic-ax  1564  2sb5  2292  2sb6  2293  2sb5rf  2300  moabs  2350  2mo2  2399  2eu7  2408  2eu8  2409  r3al  2784  r2exlem  2899  risset  2902  r19.35  2923  ralxpxfr2d  3152  reuind  3231  undif3  3695  unab  3701  inab  3702  inssdif0  3746  ssundif  3842  snss  4087  raldifsnb  4094  pwtp  4187  unipr  4203  uni0b  4215  iinuni  4358  reusv2lem4  4605  pwtr  4653  elxp2  4857  opthprc  4887  xpiundir  4895  elvvv  4899  xpsspw  4953  relun  4955  inopab  4970  difopab  4971  ralxpf  4986  dmiun  5049  inisegn0  5206  rniun  5252  cnvresima  5331  imaco  5347  mptfnf  5709  fnopabg  5711  dff1o2  5833  brprcneu  5872  idref  6164  imaiun  6168  sorpss  6595  opabex3d  6790  opabex3  6791  ovmptss  6896  fnsuppres  6961  rankc1  8359  aceq1  8566  dfac10  8585  fin41  8892  axgroth6  9271  genpass  9452  infm3  10590  prime  11039  elixx3g  11673  elfz2  11817  elfzuzb  11820  rpnnen2  14355  divalgb  14464  1nprm  14708  maxprmfct  14731  vdwmc  15007  imasleval  15525  issubm  16672  issubg3  16913  efgrelexlemb  17478  ist1-2  20440  unisngl  20619  elflim2  21057  isfcls  21102  istlm  21277  isnlm  21756  ishl2  22415  0wlk  25354  0trl  25355  erclwwlkref  25620  erclwwlknref  25632  h1de2ctlem  27289  nonbooli  27385  5oalem7  27394  ho01i  27562  rnbra  27841  cvnbtwn3  28022  chrelat2i  28099  moel  28198  uniinn0  28241  disjex  28279  maprnin  28391  ordtconlem1  28804  esum2dlem  28987  eulerpartgbij  29278  eulerpartlemr  29280  eulerpartlemn  29287  ballotlem2  29394  bnj976  29661  bnj1185  29677  bnj543  29776  bnj571  29789  bnj611  29801  bnj916  29816  bnj1000  29824  bnj1040  29853  iscvm  30054  untuni  30408  dfso3  30424  dffr5  30464  nofulllem5  30666  brtxpsd3  30734  brbigcup  30736  fixcnv  30746  ellimits  30748  elfuns  30753  brimage  30764  brcart  30770  brimg  30775  brapply  30776  brcup  30777  brcap  30778  dfrdg4  30789  dfint3  30790  ellines  30990  elicc3  31044  bj-ssb1  31310  bj-snsetex  31627  bj-snglc  31633  bj-projun  31658  bj-vjust2  31689  wl-cases2-dnf  31920  poimirlem27  32031  mblfinlem2  32042  iscrngo2  32295  prtlem70  32489  prtlem100  32493  n0el  32497  prtlem15  32511  prter2  32517  lcvnbtwn3  32665  ishlat1  32989  ishlat2  32990  hlrelat2  33039  islpln5  33171  islvol5  33215  pclclN  33527  cdleme0nex  33927  aaitgo  36099  isdomn3  36152  imaiun1  36314  relexp0eq  36364  2sbc6g  36836  2sbc5g  36837  2reu7  38757  2reu8  38758  01wlk  40005  alsconv  41035