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  1674  nfnbi  1856  2sb6  2088  2sb5  2279  dfsb7  2280  2sb5rf  2471  2sb6rf  2472  eu6lem  2567  eu6  2568  2mo2  2641  2eu7  2652  2eu8  2653  euae  2654  r2exlem  3119  r3al  3168  risset  3205  ralcom4  3256  rexcom4  3257  rabbi  3423  ralxpxfr2d  3599  reuind  3710  dfss2  3918  undif3  4248  unab  4256  inab  4257  n0el  4312  inssdif0  4322  ssundif  4436  raldifsnb  4746  pwtp  4852  uni0b  4883  iinuni  5044  inuni  5286  reusv2lem4  5337  pwtr  5391  opthprc  5678  xpiundir  5686  xpsspw  5747  relun  5749  inopab  5767  difopab  5768  ralxpf  5784  dmiun  5851  elidinxp  5990  iresn0n0  6000  inisegn0  6044  rniun  6091  imaco  6195  rnco  6196  mptfnf  6612  fnopabg  6614  dff1o2  6764  brprcneu  6807  brprcneuALT  6808  idref  7074  imaiun  7174  sorpss  7656  opabex3d  7892  opabex3rd  7893  opabex3  7894  ovmptss  8018  frpoins3xpg  8065  frpoins3xp3g  8066  poxp2  8068  poxp3  8075  fnsuppres  8116  sbthfilem  9102  ttrcltr  9601  rankc1  9755  aceq1  10000  dfac10  10021  fin41  10327  axgroth6  10711  genpass  10892  infm3  12073  prime  12546  elixx3g  13250  elfz2  13406  elfzuzb  13410  rpnnen2lem12  16126  divalgb  16307  1nprm  16582  maxprmfct  16612  vdwmc  16882  imasleval  17437  issubm  18703  issubg3  19049  efgrelexlemb  19655  isdomn5  20618  isdomn2  20619  isdomn3  20623  ist1-2  23255  unisngl  23435  elflim2  23872  isfcls  23917  istlm  24093  isnlm  24583  ishl2  25290  ovoliunlem1  25423  eln0s  28280  zaddscl  28311  readdscl  28394  remulscl  28397  erclwwlkref  29990  erclwwlknref  30039  0wlk  30086  h1de2ctlem  31525  nonbooli  31621  5oalem7  31630  ho01i  31798  rnbra  32077  cvnbtwn3  32258  chrelat2i  32335  difrab2  32467  uniinn0  32520  disjex  32562  maprnin  32704  ordtconnlem1  33927  esum2dlem  34095  eulerpartgbij  34375  eulerpartlemr  34377  eulerpartlemn  34384  ballotlem2  34492  bnj976  34779  bnj1185  34795  bnj543  34895  bnj571  34908  bnj611  34920  bnj916  34935  bnj1000  34943  bnj1040  34974  iscvm  35271  untuni  35721  dfso3  35732  dffr5  35766  elima4  35788  brtxpsd3  35909  brbigcup  35911  fixcnv  35921  ellimits  35923  elfuns  35928  brimage  35939  brcart  35945  brimg  35950  brapply  35951  brcup  35952  brcap  35953  dfrdg4  35964  dfint3  35965  ellines  36165  elicc3  36330  bj-snsetex  36976  bj-snglc  36982  bj-projun  37007  wl-2xor  37496  wl-cases2-dnf  37525  poimirlem27  37666  mblfinlem2  37677  iscrngo2  38016  n0elqs  38339  inxpxrn  38406  eqvrelcoss3  38634  prtlem70  38875  prtlem100  38877  prtlem15  38893  prter2  38899  lcvnbtwn3  39046  ishlat1  39370  ishlat2  39371  hlrelat2  39421  islpln5  39553  islvol5  39597  pclclN  39909  cdleme0nex  40308  eu6w  42688  aaitgo  43174  onmaxnelsup  43235  onsupnmax  43240  nnoeomeqom  43324  imaiun1  43663  relexp0eq  43713  ntrk1k3eqk13  44062  2sbc6g  44427  2sbc5g  44428  2reu7  47121  2reu8  47122  mosssn2  48827  iinxp  48841  ixpv  48900  alsconv  49801