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  819  pm4.78  935  xor  1017  cases2  1048  4anpull2  1363  nic-ax  1675  nfnbi  1857  2sb6  2092  2sb5  2285  dfsb7  2286  2sb5rf  2476  2sb6rf  2477  eu6lem  2573  eu6  2574  2mo2  2647  2eu7  2658  2eu8  2659  euae  2660  r2exlem  3126  r3al  3175  risset  3212  ralcom4  3263  rexcom4  3264  rabbi  3419  ralxpxfr2d  3588  reuind  3699  dfss2  3907  undif3  4240  unab  4248  inab  4249  n0el  4304  inssdif0  4314  ssundif  4427  ralf0  4437  raldifsnb  4741  pwtp  4845  uni0b  4876  iinuni  5040  inuni  5291  reusv2lem4  5343  pwtr  5404  opthprc  5695  xpiundir  5703  xpsspw  5765  relun  5767  inopab  5785  difopab  5786  ralxpf  5801  dmiun  5868  elidinxp  6009  iresn0n0  6019  inisegn0  6063  rniun  6111  imaco  6215  rnco  6216  rncoOLD  6217  mptfnf  6633  fnopabg  6635  dff1o2  6785  brprcneu  6830  brprcneuALT  6831  idref  7099  imaiun  7200  sorpss  7682  opabex3d  7918  opabex3rd  7919  opabex3  7920  ovmptss  8043  frpoins3xpg  8090  frpoins3xp3g  8091  poxp2  8093  poxp3  8100  fnsuppres  8141  sbthfilem  9132  ttrcltr  9637  rankc1  9794  aceq1  10039  dfac10  10060  fin41  10366  axgroth6  10751  genpass  10932  infm3  12115  prime  12610  elixx3g  13311  elfz2  13468  elfzuzb  13472  rpnnen2lem12  16192  divalgb  16373  1nprm  16648  maxprmfct  16679  vdwmc  16949  imasleval  17505  issubm  18771  issubg3  19120  efgrelexlemb  19725  isdomn5  20687  isdomn2  20688  isdomn3  20692  ist1-2  23312  unisngl  23492  elflim2  23929  isfcls  23974  istlm  24150  isnlm  24640  ishl2  25337  ovoliunlem1  25469  eln0s  28353  zaddscl  28386  readdscl  28491  remulscl  28494  erclwwlkref  30090  erclwwlknref  30139  0wlk  30186  h1de2ctlem  31626  nonbooli  31722  5oalem7  31731  ho01i  31899  rnbra  32178  cvnbtwn3  32359  chrelat2i  32436  difrab2  32567  uniinn0  32620  disjex  32662  maprnin  32804  ordtconnlem1  34068  esum2dlem  34236  eulerpartgbij  34516  eulerpartlemr  34518  eulerpartlemn  34525  ballotlem2  34633  bnj976  34920  bnj1185  34935  bnj543  35035  bnj571  35048  bnj611  35060  bnj916  35075  bnj1000  35083  bnj1040  35114  iscvm  35441  untuni  35891  dfso3  35902  dffr5  35936  elima4  35958  brtxpsd3  36076  brbigcup  36078  fixcnv  36088  ellimits  36090  elfuns  36095  brimage  36106  brcart  36112  brimg  36117  brapply  36118  brcup  36119  brcap  36120  dfrdg4  36133  dfint3  36134  ellines  36334  elicc3  36499  bj-snsetex  37270  bj-snglc  37276  bj-projun  37301  wl-2xor  37799  wl-cases2-dnf  37837  poimirlem27  37968  mblfinlem2  37979  iscrngo2  38318  n0elqs  38653  inxpxrn  38739  eqvrelcoss3  39023  prtlem70  39303  prtlem100  39305  prtlem15  39321  prter2  39327  lcvnbtwn3  39474  ishlat1  39798  ishlat2  39799  hlrelat2  39849  islpln5  39981  islvol5  40025  pclclN  40337  cdleme0nex  40736  eu6w  43109  aaitgo  43590  onmaxnelsup  43651  onsupnmax  43656  nnoeomeqom  43740  imaiun1  44078  relexp0eq  44128  ntrk1k3eqk13  44477  2sbc6g  44842  2sbc5g  44843  2reu7  47559  2reu8  47560  mosssn2  49292  iinxp  49306  ixpv  49365  alsconv  50265