Theorem 3bitr4ri 303

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 277	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 275	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biadan  817  pm4.78  932  xor  1012  cases2  1045  nic-ax  1667  nfnbi  1849  2sb6  2081  2sb5  2266  dfsb7  2268  2sb5rf  2465  2sb6rf  2466  eu6lem  2561  eu6  2562  2mo2  2635  2eu7  2646  2eu8  2647  euae  2648  r2exlem  3132  r3al  3186  risset  3220  ralcom4  3273  rexcom4  3275  moelOLD  3388  rabbi  3449  ralxpxfr2d  3629  reuind  3745  dfss2  3962  undif3  4289  unab  4297  inab  4298  n0el  4361  inssdif0  4371  ssundif  4489  ralf0OLD  4519  raldifsnb  4801  pwtp  4904  uniprOLD  4927  uni0b  4937  iinuni  5102  inuni  5346  reusv2lem4  5401  pwtr  5454  opthprc  5742  xpiundir  5749  xpsspw  5811  relun  5813  inopab  5831  difopab  5832  difopabOLD  5833  ralxpf  5849  dmiun  5916  elidinxp  6048  iresn0n0  6058  inisegn0  6103  rniun  6154  imaco  6257  rnco  6258  mptfnf  6691  fnopabg  6693  dff1o2  6843  brprcneu  6886  brprcneuALT  6887  idref  7155  imaiun  7255  sorpss  7734  opabex3d  7970  opabex3rd  7971  opabex3  7972  ovmptss  8098  frpoins3xpg  8145  frpoins3xp3g  8146  poxp2  8148  poxp3  8155  fnsuppres  8196  sbthfilem  9226  ttrcltr  9741  rankc1  9895  aceq1  10142  dfac10  10162  fin41  10469  axgroth6  10853  genpass  11034  infm3  12206  prime  12676  elixx3g  13372  elfz2  13526  elfzuzb  13530  rpnnen2lem12  16205  divalgb  16384  1nprm  16653  maxprmfct  16683  vdwmc  16950  imasleval  17526  issubm  18763  issubg3  19107  efgrelexlemb  19717  isdomn3  21265  isdomn5  21266  ist1-2  23295  unisngl  23475  elflim2  23912  isfcls  23957  istlm  24133  isnlm  24636  ishl2  25342  ovoliunlem1  25475  eln0s  28273  readdscl  28299  remulscl  28302  erclwwlkref  29902  erclwwlknref  29951  0wlk  29998  h1de2ctlem  31437  nonbooli  31533  5oalem7  31542  ho01i  31710  rnbra  31989  cvnbtwn3  32170  chrelat2i  32247  difrab2  32374  uniinn0  32420  disjex  32461  maprnin  32595  ordtconnlem1  33656  esum2dlem  33842  eulerpartgbij  34123  eulerpartlemr  34125  eulerpartlemn  34132  ballotlem2  34239  bnj976  34539  bnj1185  34555  bnj543  34655  bnj571  34668  bnj611  34680  bnj916  34695  bnj1000  34703  bnj1040  34734  iscvm  35000  untuni  35434  dfso3  35445  dffr5  35479  elima4  35502  brtxpsd3  35623  brbigcup  35625  fixcnv  35635  ellimits  35637  elfuns  35642  brimage  35653  brcart  35659  brimg  35664  brapply  35665  brcup  35666  brcap  35667  dfrdg4  35678  dfint3  35679  ellines  35879  elicc3  35932  bj-snsetex  36573  bj-snglc  36579  bj-projun  36604  wl-2xor  37093  wl-cases2-dnf  37110  poimirlem27  37251  mblfinlem2  37262  iscrngo2  37601  n0elqs  37928  inxpxrn  37997  eqvrelcoss3  38220  prtlem70  38459  prtlem100  38461  prtlem15  38477  prter2  38483  lcvnbtwn3  38630  ishlat1  38954  ishlat2  38955  hlrelat2  39006  islpln5  39138  islvol5  39182  pclclN  39494  cdleme0nex  39893  eu6w  42236  aaitgo  42728  onmaxnelsup  42793  onsupnmax  42798  nnoeomeqom  42883  imaiun1  43223  relexp0eq  43273  ntrk1k3eqk13  43622  2sbc6g  43994  2sbc5g  43995  2reu7  46629  2reu8  46630  mosssn2  48073  iscnrm3lem3  48140  alsconv  48409