Theorem 3bitr4ri 292

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

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  pm4.78  604  xor  931  nannan  1443  nic-ax  1589  2sb5  2431  2sb6  2432  2sb5rf  2439  moabs  2489  2mo2  2538  2eu7  2547  2eu8  2548  r3al  2924  r2exlem  3041  risset  3044  r19.35  3065  ralxpxfr2d  3298  reuind  3378  undif3  3847  undif3OLD  3848  unab  3853  inab  3854  inssdif0  3901  ssundif  4004  ralf0  4030  snss  4259  raldifsnb  4266  pwtp  4369  unipr  4385  uni0b  4399  iinuni  4545  reusv2lem4  4798  pwtr  4848  elxp2OLD  5057  opthprc  5089  xpiundir  5097  xpsspw  5156  relun  5158  inopab  5174  difopab  5175  ralxpf  5190  dmiun  5255  inisegn0  5416  rniun  5462  imaco  5557  mptfnf  5928  fnopabg  5930  dff1o2  6055  brprcneu  6096  idref  6403  imaiun  6407  sorpss  6840  opabex3d  7037  opabex3  7038  ovmptss  7145  fnsuppres  7209  rankc1  8616  aceq1  8823  dfac10  8842  fin41  9149  axgroth6  9529  genpass  9710  infm3  10861  prime  11334  elixx3g  12059  elfz2  12204  elfzuzb  12207  rpnnen2lem12  14793  divalgb  14965  1nprm  15230  maxprmfct  15259  vdwmc  15520  imasleval  16024  issubm  17170  issubg3  17435  efgrelexlemb  17986  ist1-2  20961  unisngl  21140  elflim2  21578  isfcls  21623  istlm  21798  isnlm  22289  ishl2  22974  0wlk  26075  0trl  26076  erclwwlkref  26341  erclwwlknref  26353  h1de2ctlem  27798  nonbooli  27894  5oalem7  27903  ho01i  28071  rnbra  28350  cvnbtwn3  28531  chrelat2i  28608  moel  28707  uniinn0  28749  disjex  28787  maprnin  28894  ordtconlem1  29298  esum2dlem  29481  eulerpartgbij  29761  eulerpartlemr  29763  eulerpartlemn  29770  ballotlem2  29877  bnj976  30102  bnj1185  30118  bnj543  30217  bnj571  30230  bnj611  30242  bnj916  30257  bnj1000  30265  bnj1040  30294  iscvm  30495  untuni  30840  dfso3  30856  dffr5  30896  elima4  30924  nofulllem5  31105  brtxpsd3  31173  brbigcup  31175  fixcnv  31185  ellimits  31187  elfuns  31192  brimage  31203  brcart  31209  brimg  31214  brapply  31215  brcup  31216  brcap  31217  dfrdg4  31228  dfint3  31229  ellines  31429  elicc3  31481  bj-ssb1  31822  bj-snsetex  32144  bj-snglc  32150  bj-projun  32175  bj-vjust2  32206  wl-cases2-dnf  32474  poimirlem27  32606  mblfinlem2  32617  iscrngo2  32966  prtlem70  33157  prtlem100  33161  n0el  33164  prtlem15  33178  prter2  33184  lcvnbtwn3  33333  ishlat1  33657  ishlat2  33658  hlrelat2  33707  islpln5  33839  islvol5  33883  pclclN  34195  cdleme0nex  34595  aaitgo  36751  isdomn3  36801  imaiun1  36962  relexp0eq  37012  ntrk1k3eqk13  37368  2sbc6g  37638  2sbc5g  37639  2reu7  39840  2reu8  39841  erclwwlksref  41241  erclwwlksnref  41253  01wlk  41284  alsconv  42345