Theorem 3bitr4ri 307

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 281	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 279	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biadan  818  pm4.78  932  xor  1012  cases2  1043  noranOLD  1528  nic-ax  1675  2sb6  2091  2sb5  2278  dfsb7  2281  2sb5rf  2485  2sb6rf  2486  eu6lem  2633  eu6  2634  2mo2  2709  2eu7  2720  2eu8  2721  euae  2722  r3al  3167  risset  3226  r2exlem  3261  ralxpxfr2d  3587  reuind  3692  undif3  4215  unab  4222  inab  4223  n0el  4275  inssdif0  4283  ssundif  4391  ralf0  4415  raldifsnb  4689  pwtp  4795  unipr  4817  uni0b  4826  iinuni  4983  reusv2lem4  5267  pwtr  5310  opthprc  5580  xpiundir  5587  xpsspw  5646  relun  5648  inopab  5665  difopab  5666  ralxpf  5681  dmiun  5746  elidinxp  5878  iresn0n0  5890  inisegn0  5928  rniun  5973  imaco  6071  rnco  6072  mptfnf  6455  fnopabg  6457  dff1o2  6595  brprcneu  6637  idref  6885  imaiun  6982  sorpss  7434  opabex3d  7648  opabex3rd  7649  opabex3  7650  ovmptss  7771  fnsuppres  7840  rankc1  9283  aceq1  9528  dfac10  9548  fin41  9855  axgroth6  10239  genpass  10420  infm3  11587  prime  12051  elixx3g  12739  elfz2  12892  elfzuzb  12896  rpnnen2lem12  15570  divalgb  15745  1nprm  16013  maxprmfct  16043  vdwmc  16304  imasleval  16806  issubm  17960  issubg3  18289  efgrelexlemb  18868  ist1-2  21952  unisngl  22132  elflim2  22569  isfcls  22614  istlm  22790  isnlm  23281  ishl2  23974  ovoliunlem1  24106  erclwwlkref  27805  erclwwlknref  27854  0wlk  27901  h1de2ctlem  29338  nonbooli  29434  5oalem7  29443  ho01i  29611  rnbra  29890  cvnbtwn3  30071  chrelat2i  30148  nelbOLD  30239  moel  30259  difrab2  30268  uniinn0  30314  disjex  30355  maprnin  30493  ordtconnlem1  31277  esum2dlem  31461  eulerpartgbij  31740  eulerpartlemr  31742  eulerpartlemn  31749  ballotlem2  31856  bnj976  32159  bnj1185  32175  bnj543  32275  bnj571  32288  bnj611  32300  bnj916  32315  bnj1000  32323  bnj1040  32354  iscvm  32619  untuni  33048  dfso3  33063  dffr5  33102  elima4  33132  brtxpsd3  33470  brbigcup  33472  fixcnv  33482  ellimits  33484  elfuns  33489  brimage  33500  brcart  33506  brimg  33511  brapply  33512  brcup  33513  brcap  33514  dfrdg4  33525  dfint3  33526  ellines  33726  elicc3  33778  bj-snsetex  34399  bj-snglc  34405  bj-projun  34430  bj-vjust  34470  wl-2xor  34900  wl-cases2-dnf  34917  poimirlem27  35084  mblfinlem2  35095  iscrngo2  35435  n0elqs  35743  inxpxrn  35803  eqvrelcoss3  36013  prtlem70  36153  prtlem100  36155  prtlem15  36171  prter2  36177  lcvnbtwn3  36324  ishlat1  36648  ishlat2  36649  hlrelat2  36699  islpln5  36831  islvol5  36875  pclclN  37187  cdleme0nex  37586  aaitgo  40106  isdomn3  40148  imaiun1  40352  relexp0eq  40402  ntrk1k3eqk13  40753  2sbc6g  41119  2sbc5g  41120  2reu7  43667  2reu8  43668  alsconv  45318