Theorem 3bitr4ri 293

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  pm4.78  606  xor  935  nannan  1451  nic-ax  1598  2sb5  2443  2sb6  2444  2sb5rf  2451  moabs  2501  2mo2  2550  2eu7  2559  2eu8  2560  r3al  2940  r2exlem  3059  risset  3062  r19.35  3084  ralxpxfr2d  3327  reuind  3411  undif3  3888  undif3OLD  3889  unab  3894  inab  3895  n0el  3940  inssdif0  3947  ssundif  4052  ralf0  4078  snss  4316  raldifsnb  4325  pwtp  4431  unipr  4449  uni0b  4463  iinuni  4609  reusv2lem4  4872  pwtr  4921  elxp2OLD  5133  opthprc  5167  xpiundir  5174  xpsspw  5233  relun  5235  inopab  5252  difopab  5253  ralxpf  5268  dmiun  5333  inisegn0  5497  rniun  5543  imaco  5640  mptfnf  6015  fnopabg  6017  dff1o2  6142  brprcneu  6184  idref  6499  imaiun  6503  sorpss  6942  opabex3d  7145  opabex3  7146  ovmptss  7258  fnsuppres  7322  rankc1  8733  aceq1  8940  dfac10  8959  fin41  9266  axgroth6  9650  genpass  9831  infm3  10982  prime  11458  elixx3g  12188  elfz2  12333  elfzuzb  12336  rpnnen2lem12  14954  divalgb  15127  1nprm  15392  maxprmfct  15421  vdwmc  15682  imasleval  16201  issubm  17347  issubg3  17612  efgrelexlemb  18163  ist1-2  21151  unisngl  21330  elflim2  21768  isfcls  21813  istlm  21988  isnlm  22479  ishl2  23166  erclwwlksref  26934  erclwwlksnref  26946  0wlk  26977  h1de2ctlem  28414  nonbooli  28510  5oalem7  28519  ho01i  28687  rnbra  28966  cvnbtwn3  29147  chrelat2i  29224  moel  29323  difrab2  29339  uniinn0  29366  disjex  29405  maprnin  29506  ordtconnlem1  29970  esum2dlem  30154  eulerpartgbij  30434  eulerpartlemr  30436  eulerpartlemn  30443  ballotlem2  30550  bnj976  30848  bnj1185  30864  bnj543  30963  bnj571  30976  bnj611  30988  bnj916  31003  bnj1000  31011  bnj1040  31040  iscvm  31241  untuni  31586  dfso3  31601  dffr5  31643  elima4  31679  brtxpsd3  32003  brbigcup  32005  fixcnv  32015  ellimits  32017  elfuns  32022  brimage  32033  brcart  32039  brimg  32044  brapply  32045  brcup  32046  brcap  32047  dfrdg4  32058  dfint3  32059  ellines  32259  elicc3  32311  bj-ssb1  32633  bj-snsetex  32951  bj-snglc  32957  bj-projun  32982  bj-vjust2  33015  wl-cases2-dnf  33295  poimirlem27  33436  mblfinlem2  33447  iscrngo2  33796  ralanid  34010  n0elqs  34098  prtlem70  34141  prtlem100  34144  prtlem15  34160  prter2  34166  lcvnbtwn3  34315  ishlat1  34639  ishlat2  34640  hlrelat2  34689  islpln5  34821  islvol5  34865  pclclN  35177  cdleme0nex  35577  aaitgo  37732  isdomn3  37782  imaiun1  37943  relexp0eq  37993  ntrk1k3eqk13  38348  2sbc6g  38616  2sbc5g  38617  2reu7  41191  2reu8  41192  alsconv  42536