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  2091  2sb5  2284  dfsb7  2285  2sb5rf  2476  2sb6rf  2477  eu6lem  2573  eu6  2574  2mo2  2647  2eu7  2658  2eu8  2659  euae  2660  r2exlem  3125  r3al  3174  risset  3211  ralcom4  3262  rexcom4  3263  rabbi  3429  ralxpxfr2d  3600  reuind  3711  dfss2  3919  undif3  4252  unab  4260  inab  4261  n0el  4316  inssdif0  4326  ssundif  4440  ralf0  4450  raldifsnb  4752  pwtp  4858  uni0b  4889  iinuni  5053  inuni  5295  reusv2lem4  5346  pwtr  5400  opthprc  5688  xpiundir  5696  xpsspw  5758  relun  5760  inopab  5778  difopab  5779  ralxpf  5795  dmiun  5862  elidinxp  6003  iresn0n0  6013  inisegn0  6057  rniun  6105  imaco  6209  rnco  6210  rncoOLD  6211  mptfnf  6627  fnopabg  6629  dff1o2  6779  brprcneu  6824  brprcneuALT  6825  idref  7091  imaiun  7191  sorpss  7673  opabex3d  7909  opabex3rd  7910  opabex3  7911  ovmptss  8035  frpoins3xpg  8082  frpoins3xp3g  8083  poxp2  8085  poxp3  8092  fnsuppres  8133  sbthfilem  9122  ttrcltr  9625  rankc1  9782  aceq1  10027  dfac10  10048  fin41  10354  axgroth6  10739  genpass  10920  infm3  12101  prime  12573  elixx3g  13274  elfz2  13430  elfzuzb  13434  rpnnen2lem12  16150  divalgb  16331  1nprm  16606  maxprmfct  16636  vdwmc  16906  imasleval  17462  issubm  18728  issubg3  19074  efgrelexlemb  19679  isdomn5  20643  isdomn2  20644  isdomn3  20648  ist1-2  23291  unisngl  23471  elflim2  23908  isfcls  23953  istlm  24129  isnlm  24619  ishl2  25326  ovoliunlem1  25459  eln0s  28357  zaddscl  28390  readdscl  28495  remulscl  28498  erclwwlkref  30095  erclwwlknref  30144  0wlk  30191  h1de2ctlem  31630  nonbooli  31726  5oalem7  31735  ho01i  31903  rnbra  32182  cvnbtwn3  32363  chrelat2i  32440  difrab2  32572  uniinn0  32625  disjex  32667  maprnin  32810  ordtconnlem1  34081  esum2dlem  34249  eulerpartgbij  34529  eulerpartlemr  34531  eulerpartlemn  34538  ballotlem2  34646  bnj976  34933  bnj1185  34949  bnj543  35049  bnj571  35062  bnj611  35074  bnj916  35089  bnj1000  35097  bnj1040  35128  iscvm  35453  untuni  35903  dfso3  35914  dffr5  35948  elima4  35970  brtxpsd3  36088  brbigcup  36090  fixcnv  36100  ellimits  36102  elfuns  36107  brimage  36118  brcart  36124  brimg  36129  brapply  36130  brcup  36131  brcap  36132  dfrdg4  36145  dfint3  36146  ellines  36346  elicc3  36511  bj-snsetex  37164  bj-snglc  37170  bj-projun  37195  wl-2xor  37688  wl-cases2-dnf  37717  poimirlem27  37848  mblfinlem2  37859  iscrngo2  38198  n0elqs  38525  inxpxrn  38603  eqvrelcoss3  38875  prtlem70  39117  prtlem100  39119  prtlem15  39135  prter2  39141  lcvnbtwn3  39288  ishlat1  39612  ishlat2  39613  hlrelat2  39663  islpln5  39795  islvol5  39839  pclclN  40151  cdleme0nex  40550  eu6w  42919  aaitgo  43404  onmaxnelsup  43465  onsupnmax  43470  nnoeomeqom  43554  imaiun1  43892  relexp0eq  43942  ntrk1k3eqk13  44291  2sbc6g  44656  2sbc5g  44657  2reu7  47357  2reu8  47358  mosssn2  49062  iinxp  49076  ixpv  49135  alsconv  50035