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  1362  nic-ax  1673  nfnbi  1855  2sb6  2086  2sb5  2278  dfsb7  2279  2sb5rf  2477  2sb6rf  2478  eu6lem  2573  eu6  2574  2mo2  2647  2eu7  2658  2eu8  2659  euae  2660  r2exlem  3143  r3al  3197  risset  3233  ralcom4  3286  rexcom4  3288  moelOLD  3405  rabbi  3467  ralxpxfr2d  3646  reuind  3759  dfss2  3969  undif3  4300  unab  4308  inab  4309  n0el  4364  inssdif0  4374  ssundif  4488  raldifsnb  4796  pwtp  4902  uni0b  4933  iinuni  5098  inuni  5350  reusv2lem4  5401  pwtr  5457  opthprc  5749  xpiundir  5757  xpsspw  5819  relun  5821  inopab  5839  difopab  5840  difopabOLD  5841  ralxpf  5857  dmiun  5924  elidinxp  6062  iresn0n0  6072  inisegn0  6116  rniun  6167  imaco  6271  rnco  6272  mptfnf  6703  fnopabg  6705  dff1o2  6853  brprcneu  6896  brprcneuALT  6897  idref  7166  imaiun  7265  sorpss  7748  opabex3d  7990  opabex3rd  7991  opabex3  7992  ovmptss  8118  frpoins3xpg  8165  frpoins3xp3g  8166  poxp2  8168  poxp3  8175  fnsuppres  8216  sbthfilem  9238  ttrcltr  9756  rankc1  9910  aceq1  10157  dfac10  10178  fin41  10484  axgroth6  10868  genpass  11049  infm3  12227  prime  12699  elixx3g  13400  elfz2  13554  elfzuzb  13558  rpnnen2lem12  16261  divalgb  16441  1nprm  16716  maxprmfct  16746  vdwmc  17016  imasleval  17586  issubm  18816  issubg3  19162  efgrelexlemb  19768  isdomn5  20710  isdomn2  20711  isdomn3  20715  ist1-2  23355  unisngl  23535  elflim2  23972  isfcls  24017  istlm  24193  isnlm  24696  ishl2  25404  ovoliunlem1  25537  eln0s  28358  zaddscl  28380  readdscl  28431  remulscl  28434  erclwwlkref  30039  erclwwlknref  30088  0wlk  30135  h1de2ctlem  31574  nonbooli  31670  5oalem7  31679  ho01i  31847  rnbra  32126  cvnbtwn3  32307  chrelat2i  32384  difrab2  32517  uniinn0  32563  disjex  32605  maprnin  32742  ordtconnlem1  33923  esum2dlem  34093  eulerpartgbij  34374  eulerpartlemr  34376  eulerpartlemn  34383  ballotlem2  34491  bnj976  34791  bnj1185  34807  bnj543  34907  bnj571  34920  bnj611  34932  bnj916  34947  bnj1000  34955  bnj1040  34986  iscvm  35264  untuni  35709  dfso3  35720  dffr5  35754  elima4  35776  brtxpsd3  35897  brbigcup  35899  fixcnv  35909  ellimits  35911  elfuns  35916  brimage  35927  brcart  35933  brimg  35938  brapply  35939  brcup  35940  brcap  35941  dfrdg4  35952  dfint3  35953  ellines  36153  elicc3  36318  bj-snsetex  36964  bj-snglc  36970  bj-projun  36995  wl-2xor  37484  wl-cases2-dnf  37513  poimirlem27  37654  mblfinlem2  37665  iscrngo2  38004  n0elqs  38327  inxpxrn  38396  eqvrelcoss3  38619  prtlem70  38858  prtlem100  38860  prtlem15  38876  prter2  38882  lcvnbtwn3  39029  ishlat1  39353  ishlat2  39354  hlrelat2  39405  islpln5  39537  islvol5  39581  pclclN  39893  cdleme0nex  40292  eu6w  42686  aaitgo  43174  onmaxnelsup  43235  onsupnmax  43240  nnoeomeqom  43325  imaiun1  43664  relexp0eq  43714  ntrk1k3eqk13  44063  2sbc6g  44434  2sbc5g  44435  2reu7  47123  2reu8  47124  mosssn2  48736  alsconv  49309