Theorem 3bitr4ri 282

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

Syntax hints:   <-> wb 188

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 189

This theorem is referenced by:  pm4.78  586  xor  902  nannan  1389  nanbiOLDOLD  1395  nic-ax  1556  2sb5  2272  2sb6  2273  2sb5rf  2280  moabs  2330  2mo2  2379  2eu7  2388  2eu8  2389  r3al  2768  r2exlem  2910  risset  2915  r19.35  2937  ralxpxfr2d  3164  reuind  3243  undif3  3704  unab  3710  inab  3711  inssdif0  3834  ssundif  3851  snss  4096  raldifsnb  4103  pwtp  4195  unipr  4211  uni0b  4223  iinuni  4365  reusv2lem4  4607  pwtr  4653  elxp2  4852  opthprc  4882  xpiundir  4890  elvvv  4894  xpsspw  4948  relun  4950  inopab  4965  difopab  4966  ralxpf  4981  dmiun  5043  inisegn0  5200  rniun  5246  cnvresima  5324  imaco  5340  mptfnf  5699  fnopabg  5701  dff1o2  5819  brprcneu  5858  idref  6146  imaiun  6150  sorpss  6576  opabex3d  6771  opabex3  6772  ovmptss  6877  fnsuppres  6942  rankc1  8341  aceq1  8548  dfac10  8567  fin41  8874  axgroth6  9253  genpass  9434  infm3  10568  prime  11016  elixx3g  11648  elfz2  11791  elfzuzb  11794  rpnnen2  14278  divalgb  14385  1nprm  14629  maxprmfct  14652  vdwmc  14928  imasleval  15447  issubm  16594  issubg3  16835  efgrelexlemb  17400  ist1-2  20363  unisngl  20542  elflim2  20979  isfcls  21024  istlm  21199  isnlm  21678  ishl2  22337  0wlk  25275  0trl  25276  erclwwlkref  25541  erclwwlknref  25553  h1de2ctlem  27208  nonbooli  27304  5oalem7  27313  ho01i  27481  rnbra  27760  cvnbtwn3  27941  chrelat2i  28018  moel  28119  uniinn0  28163  disjex  28202  maprnin  28316  ordtconlem1  28730  esum2dlem  28913  eulerpartgbij  29205  eulerpartlemr  29207  eulerpartlemn  29214  ballotlem2  29321  bnj976  29589  bnj1185  29605  bnj543  29704  bnj571  29717  bnj611  29729  bnj916  29744  bnj1000  29752  bnj1040  29781  iscvm  29982  untuni  30336  dfso3  30352  dffr5  30393  nofulllem5  30595  brtxpsd3  30663  brbigcup  30665  fixcnv  30675  ellimits  30677  elfuns  30682  brimage  30693  brcart  30699  brimg  30704  brapply  30705  brcup  30706  brcap  30707  dfrdg4  30718  dfint3  30719  ellines  30919  elicc3  30973  bj-ssb1  31246  bj-snsetex  31557  bj-snglc  31563  bj-projun  31588  bj-vjust2  31619  wl-cases2-dnf  31850  poimirlem27  31967  mblfinlem2  31978  iscrngo2  32231  prtlem70  32425  prtlem100  32429  n0el  32433  prtlem15  32447  prter2  32453  lcvnbtwn3  32594  ishlat1  32918  ishlat2  32919  hlrelat2  32968  islpln5  33100  islvol5  33144  pclclN  33456  cdleme0nex  33856  aaitgo  36028  isdomn3  36081  imaiun1  36243  relexp0eq  36293  2sbc6g  36766  2sbc5g  36767  2reu7  38612  2reu8  38613  01wlk  39704  alsconv  40582