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  934  xor  1016  cases2  1047  4anpull2  1362  nic-ax  1673  nfnbi  1855  2sb6  2087  2sb5  2278  dfsb7  2279  2sb5rf  2470  2sb6rf  2471  eu6lem  2566  eu6  2567  2mo2  2640  2eu7  2651  2eu8  2652  euae  2653  r2exlem  3118  r3al  3167  risset  3204  ralcom4  3255  rexcom4  3256  rabbi  3427  ralxpxfr2d  3603  reuind  3715  dfss2  3923  undif3  4253  unab  4261  inab  4262  n0el  4317  inssdif0  4327  ssundif  4441  raldifsnb  4750  pwtp  4856  uni0b  4887  iinuni  5050  inuni  5292  reusv2lem4  5343  pwtr  5399  opthprc  5687  xpiundir  5695  xpsspw  5756  relun  5758  inopab  5776  difopab  5777  ralxpf  5793  dmiun  5860  elidinxp  5999  iresn0n0  6009  inisegn0  6053  rniun  6100  imaco  6204  rnco  6205  mptfnf  6621  fnopabg  6623  dff1o2  6773  brprcneu  6816  brprcneuALT  6817  idref  7084  imaiun  7185  sorpss  7668  opabex3d  7907  opabex3rd  7908  opabex3  7909  ovmptss  8033  frpoins3xpg  8080  frpoins3xp3g  8081  poxp2  8083  poxp3  8090  fnsuppres  8131  sbthfilem  9122  ttrcltr  9631  rankc1  9785  aceq1  10030  dfac10  10051  fin41  10357  axgroth6  10741  genpass  10922  infm3  12102  prime  12575  elixx3g  13279  elfz2  13435  elfzuzb  13439  rpnnen2lem12  16152  divalgb  16333  1nprm  16608  maxprmfct  16638  vdwmc  16908  imasleval  17463  issubm  18695  issubg3  19041  efgrelexlemb  19647  isdomn5  20613  isdomn2  20614  isdomn3  20618  ist1-2  23250  unisngl  23430  elflim2  23867  isfcls  23912  istlm  24088  isnlm  24579  ishl2  25286  ovoliunlem1  25419  eln0s  28274  zaddscl  28305  readdscl  28386  remulscl  28389  erclwwlkref  29982  erclwwlknref  30031  0wlk  30078  h1de2ctlem  31517  nonbooli  31613  5oalem7  31622  ho01i  31790  rnbra  32069  cvnbtwn3  32250  chrelat2i  32327  difrab2  32460  uniinn0  32512  disjex  32554  maprnin  32687  ordtconnlem1  33893  esum2dlem  34061  eulerpartgbij  34342  eulerpartlemr  34344  eulerpartlemn  34351  ballotlem2  34459  bnj976  34746  bnj1185  34762  bnj543  34862  bnj571  34875  bnj611  34887  bnj916  34902  bnj1000  34910  bnj1040  34941  iscvm  35234  untuni  35684  dfso3  35695  dffr5  35729  elima4  35751  brtxpsd3  35872  brbigcup  35874  fixcnv  35884  ellimits  35886  elfuns  35891  brimage  35902  brcart  35908  brimg  35913  brapply  35914  brcup  35915  brcap  35916  dfrdg4  35927  dfint3  35928  ellines  36128  elicc3  36293  bj-snsetex  36939  bj-snglc  36945  bj-projun  36970  wl-2xor  37459  wl-cases2-dnf  37488  poimirlem27  37629  mblfinlem2  37640  iscrngo2  37979  n0elqs  38302  inxpxrn  38369  eqvrelcoss3  38597  prtlem70  38838  prtlem100  38840  prtlem15  38856  prter2  38862  lcvnbtwn3  39009  ishlat1  39333  ishlat2  39334  hlrelat2  39385  islpln5  39517  islvol5  39561  pclclN  39873  cdleme0nex  40272  eu6w  42652  aaitgo  43138  onmaxnelsup  43199  onsupnmax  43204  nnoeomeqom  43288  imaiun1  43627  relexp0eq  43677  ntrk1k3eqk13  44026  2sbc6g  44391  2sbc5g  44392  2reu7  47099  2reu8  47100  mosssn2  48805  iinxp  48819  ixpv  48878  alsconv  49779