Theorem 3bitr4ri 304

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 278	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 276	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  biadan  818  pm4.78  933  xor  1015  cases2  1048  nic-ax  1671  nfnbi  1853  2sb6  2086  2sb5  2281  dfsb7  2283  2sb5rf  2480  2sb6rf  2481  eu6lem  2576  eu6  2577  2mo2  2650  2eu7  2661  2eu8  2662  euae  2663  r2exlem  3149  r3al  3203  risset  3239  ralcom4  3292  rexcom4  3294  moelOLD  3413  rabbi  3475  ralxpxfr2d  3659  reuind  3775  dfss2  3994  undif3  4319  unab  4327  inab  4328  n0el  4387  inssdif0  4397  ssundif  4511  raldifsnb  4821  pwtp  4926  uni0b  4957  iinuni  5121  inuni  5368  reusv2lem4  5419  pwtr  5472  opthprc  5764  xpiundir  5771  xpsspw  5833  relun  5835  inopab  5853  difopab  5854  difopabOLD  5855  ralxpf  5871  dmiun  5938  elidinxp  6073  iresn0n0  6083  inisegn0  6128  rniun  6179  imaco  6282  rnco  6283  mptfnf  6715  fnopabg  6717  dff1o2  6867  brprcneu  6910  brprcneuALT  6911  idref  7180  imaiun  7282  sorpss  7763  opabex3d  8006  opabex3rd  8007  opabex3  8008  ovmptss  8134  frpoins3xpg  8181  frpoins3xp3g  8182  poxp2  8184  poxp3  8191  fnsuppres  8232  sbthfilem  9264  ttrcltr  9785  rankc1  9939  aceq1  10186  dfac10  10207  fin41  10513  axgroth6  10897  genpass  11078  infm3  12254  prime  12724  elixx3g  13420  elfz2  13574  elfzuzb  13578  rpnnen2lem12  16273  divalgb  16452  1nprm  16726  maxprmfct  16756  vdwmc  17025  imasleval  17601  issubm  18838  issubg3  19184  efgrelexlemb  19792  isdomn5  20732  isdomn2  20733  isdomn3  20737  ist1-2  23376  unisngl  23556  elflim2  23993  isfcls  24038  istlm  24214  isnlm  24717  ishl2  25423  ovoliunlem1  25556  eln0s  28376  zaddscl  28398  readdscl  28449  remulscl  28452  erclwwlkref  30052  erclwwlknref  30101  0wlk  30148  h1de2ctlem  31587  nonbooli  31683  5oalem7  31692  ho01i  31860  rnbra  32139  cvnbtwn3  32320  chrelat2i  32397  difrab2  32526  uniinn0  32573  disjex  32614  maprnin  32745  ordtconnlem1  33870  esum2dlem  34056  eulerpartgbij  34337  eulerpartlemr  34339  eulerpartlemn  34346  ballotlem2  34453  bnj976  34753  bnj1185  34769  bnj543  34869  bnj571  34882  bnj611  34894  bnj916  34909  bnj1000  34917  bnj1040  34948  iscvm  35227  untuni  35671  dfso3  35682  dffr5  35716  elima4  35739  brtxpsd3  35860  brbigcup  35862  fixcnv  35872  ellimits  35874  elfuns  35879  brimage  35890  brcart  35896  brimg  35901  brapply  35902  brcup  35903  brcap  35904  dfrdg4  35915  dfint3  35916  ellines  36116  elicc3  36283  bj-snsetex  36929  bj-snglc  36935  bj-projun  36960  wl-2xor  37449  wl-cases2-dnf  37466  poimirlem27  37607  mblfinlem2  37618  iscrngo2  37957  n0elqs  38282  inxpxrn  38351  eqvrelcoss3  38574  prtlem70  38813  prtlem100  38815  prtlem15  38831  prter2  38837  lcvnbtwn3  38984  ishlat1  39308  ishlat2  39309  hlrelat2  39360  islpln5  39492  islvol5  39536  pclclN  39848  cdleme0nex  40247  eu6w  42631  aaitgo  43119  onmaxnelsup  43184  onsupnmax  43189  nnoeomeqom  43274  imaiun1  43613  relexp0eq  43663  ntrk1k3eqk13  44012  2sbc6g  44384  2sbc5g  44385  2reu7  47026  2reu8  47027  mosssn2  48548  iscnrm3lem3  48615  alsconv  48884