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  2477  2sb6rf  2478  eu6lem  2574  eu6  2575  2mo2  2648  2eu7  2659  2eu8  2660  euae  2661  r2exlem  3127  r3al  3176  risset  3213  ralcom4  3264  rexcom4  3265  rabbi  3431  ralxpxfr2d  3602  reuind  3713  dfss2  3921  undif3  4254  unab  4262  inab  4263  n0el  4318  inssdif0  4328  ssundif  4442  ralf0  4452  raldifsnb  4754  pwtp  4860  uni0b  4891  iinuni  5055  inuni  5297  reusv2lem4  5348  pwtr  5407  opthprc  5696  xpiundir  5704  xpsspw  5766  relun  5768  inopab  5786  difopab  5787  ralxpf  5803  dmiun  5870  elidinxp  6011  iresn0n0  6021  inisegn0  6065  rniun  6113  imaco  6217  rnco  6218  rncoOLD  6219  mptfnf  6635  fnopabg  6637  dff1o2  6787  brprcneu  6832  brprcneuALT  6833  idref  7101  imaiun  7201  sorpss  7683  opabex3d  7919  opabex3rd  7920  opabex3  7921  ovmptss  8045  frpoins3xpg  8092  frpoins3xp3g  8093  poxp2  8095  poxp3  8102  fnsuppres  8143  sbthfilem  9134  ttrcltr  9637  rankc1  9794  aceq1  10039  dfac10  10060  fin41  10366  axgroth6  10751  genpass  10932  infm3  12113  prime  12585  elixx3g  13286  elfz2  13442  elfzuzb  13446  rpnnen2lem12  16162  divalgb  16343  1nprm  16618  maxprmfct  16648  vdwmc  16918  imasleval  17474  issubm  18740  issubg3  19086  efgrelexlemb  19691  isdomn5  20655  isdomn2  20656  isdomn3  20660  ist1-2  23303  unisngl  23483  elflim2  23920  isfcls  23965  istlm  24141  isnlm  24631  ishl2  25338  ovoliunlem1  25471  eln0s  28369  zaddscl  28402  readdscl  28507  remulscl  28510  erclwwlkref  30107  erclwwlknref  30156  0wlk  30203  h1de2ctlem  31642  nonbooli  31738  5oalem7  31747  ho01i  31915  rnbra  32194  cvnbtwn3  32375  chrelat2i  32452  difrab2  32583  uniinn0  32636  disjex  32678  maprnin  32820  ordtconnlem1  34101  esum2dlem  34269  eulerpartgbij  34549  eulerpartlemr  34551  eulerpartlemn  34558  ballotlem2  34666  bnj976  34953  bnj1185  34968  bnj543  35068  bnj571  35081  bnj611  35093  bnj916  35108  bnj1000  35116  bnj1040  35147  iscvm  35472  untuni  35922  dfso3  35933  dffr5  35967  elima4  35989  brtxpsd3  36107  brbigcup  36109  fixcnv  36119  ellimits  36121  elfuns  36126  brimage  36137  brcart  36143  brimg  36148  brapply  36149  brcup  36150  brcap  36151  dfrdg4  36164  dfint3  36165  ellines  36365  elicc3  36530  bj-snsetex  37208  bj-snglc  37214  bj-projun  37239  wl-2xor  37735  wl-cases2-dnf  37764  poimirlem27  37895  mblfinlem2  37906  iscrngo2  38245  n0elqs  38580  inxpxrn  38666  eqvrelcoss3  38950  prtlem70  39230  prtlem100  39232  prtlem15  39248  prter2  39254  lcvnbtwn3  39401  ishlat1  39725  ishlat2  39726  hlrelat2  39776  islpln5  39908  islvol5  39952  pclclN  40264  cdleme0nex  40663  eu6w  43031  aaitgo  43516  onmaxnelsup  43577  onsupnmax  43582  nnoeomeqom  43666  imaiun1  44004  relexp0eq  44054  ntrk1k3eqk13  44403  2sbc6g  44768  2sbc5g  44769  2reu7  47468  2reu8  47469  mosssn2  49173  iinxp  49187  ixpv  49246  alsconv  50146