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  2086  2sb5  2278  dfsb7  2279  2sb5rf  2476  2sb6rf  2477  eu6lem  2572  eu6  2573  2mo2  2646  2eu7  2657  2eu8  2658  euae  2659  r2exlem  3129  r3al  3182  risset  3217  ralcom4  3268  rexcom4  3269  moelOLD  3384  rabbi  3446  ralxpxfr2d  3625  reuind  3736  dfss2  3944  undif3  4275  unab  4283  inab  4284  n0el  4339  inssdif0  4349  ssundif  4463  raldifsnb  4772  pwtp  4878  uni0b  4909  iinuni  5074  inuni  5320  reusv2lem4  5371  pwtr  5427  opthprc  5718  xpiundir  5726  xpsspw  5788  relun  5790  inopab  5808  difopab  5809  difopabOLD  5810  ralxpf  5826  dmiun  5893  elidinxp  6031  iresn0n0  6041  inisegn0  6085  rniun  6136  imaco  6240  rnco  6241  mptfnf  6672  fnopabg  6674  dff1o2  6822  brprcneu  6865  brprcneuALT  6866  idref  7135  imaiun  7236  sorpss  7720  opabex3d  7962  opabex3rd  7963  opabex3  7964  ovmptss  8090  frpoins3xpg  8137  frpoins3xp3g  8138  poxp2  8140  poxp3  8147  fnsuppres  8188  sbthfilem  9210  ttrcltr  9728  rankc1  9882  aceq1  10129  dfac10  10150  fin41  10456  axgroth6  10840  genpass  11021  infm3  12199  prime  12672  elixx3g  13373  elfz2  13529  elfzuzb  13533  rpnnen2lem12  16241  divalgb  16421  1nprm  16696  maxprmfct  16726  vdwmc  16996  imasleval  17553  issubm  18779  issubg3  19125  efgrelexlemb  19729  isdomn5  20668  isdomn2  20669  isdomn3  20673  ist1-2  23283  unisngl  23463  elflim2  23900  isfcls  23945  istlm  24121  isnlm  24612  ishl2  25320  ovoliunlem1  25453  eln0s  28275  zaddscl  28297  readdscl  28348  remulscl  28351  erclwwlkref  29947  erclwwlknref  29996  0wlk  30043  h1de2ctlem  31482  nonbooli  31578  5oalem7  31587  ho01i  31755  rnbra  32034  cvnbtwn3  32215  chrelat2i  32292  difrab2  32425  uniinn0  32477  disjex  32519  maprnin  32654  ordtconnlem1  33901  esum2dlem  34069  eulerpartgbij  34350  eulerpartlemr  34352  eulerpartlemn  34359  ballotlem2  34467  bnj976  34754  bnj1185  34770  bnj543  34870  bnj571  34883  bnj611  34895  bnj916  34910  bnj1000  34918  bnj1040  34949  iscvm  35227  untuni  35672  dfso3  35683  dffr5  35717  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  36281  bj-snsetex  36927  bj-snglc  36933  bj-projun  36958  wl-2xor  37447  wl-cases2-dnf  37476  poimirlem27  37617  mblfinlem2  37628  iscrngo2  37967  n0elqs  38290  inxpxrn  38359  eqvrelcoss3  38582  prtlem70  38821  prtlem100  38823  prtlem15  38839  prter2  38845  lcvnbtwn3  38992  ishlat1  39316  ishlat2  39317  hlrelat2  39368  islpln5  39500  islvol5  39544  pclclN  39856  cdleme0nex  40255  eu6w  42646  aaitgo  43133  onmaxnelsup  43194  onsupnmax  43199  nnoeomeqom  43283  imaiun1  43622  relexp0eq  43672  ntrk1k3eqk13  44021  2sbc6g  44387  2sbc5g  44388  2reu7  47088  2reu8  47089  mosssn2  48743  iinxp  48757  ixpv  48813  alsconv  49602