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  815  pm4.78  931  xor  1011  cases2  1044  noranOLD  1529  nic-ax  1677  nfnbi  1858  2sb6  2090  2sb5  2275  dfsb7  2279  2sb5rf  2472  2sb6rf  2473  eu6lem  2573  eu6  2574  2mo2  2649  2eu7  2659  2eu8  2660  euae  2661  r3al  3125  ralcom4  3161  rexcom4  3179  risset  3193  r2exlem  3230  moel  3349  ralxpxfr2d  3568  reuind  3683  undif3  4221  unab  4229  inab  4230  n0el  4292  inssdif0  4300  ab0  4305  ssundif  4415  ralf0OLD  4445  raldifsnb  4726  pwtp  4831  uniprOLD  4855  uni0b  4864  iinuni  5023  reusv2lem4  5319  pwtr  5362  opthprc  5642  xpiundir  5649  xpsspw  5708  relun  5710  inopab  5728  difopab  5729  ralxpf  5744  dmiun  5811  elidinxp  5940  iresn0n0  5952  inisegn0  5995  rniun  6040  imaco  6144  rnco  6145  mptfnf  6552  fnopabg  6554  dff1o2  6705  brprcneu  6747  fvprc  6748  idref  7000  imaiun  7100  sorpss  7559  opabex3d  7781  opabex3rd  7782  opabex3  7783  ovmptss  7904  fnsuppres  7978  sbthfilem  8941  rankc1  9559  aceq1  9804  dfac10  9824  fin41  10131  axgroth6  10515  genpass  10696  infm3  11864  prime  12331  elixx3g  13021  elfz2  13175  elfzuzb  13179  rpnnen2lem12  15862  divalgb  16041  1nprm  16312  maxprmfct  16342  vdwmc  16607  imasleval  17169  issubm  18357  issubg3  18688  efgrelexlemb  19271  ist1-2  22406  unisngl  22586  elflim2  23023  isfcls  23068  istlm  23244  isnlm  23745  ishl2  24439  ovoliunlem1  24571  erclwwlkref  28285  erclwwlknref  28334  0wlk  28381  h1de2ctlem  29818  nonbooli  29914  5oalem7  29923  ho01i  30091  rnbra  30370  cvnbtwn3  30551  chrelat2i  30628  nelbOLDOLD  30718  difrab2  30746  uniinn0  30791  disjex  30832  maprnin  30968  ordtconnlem1  31776  esum2dlem  31960  eulerpartgbij  32239  eulerpartlemr  32241  eulerpartlemn  32248  ballotlem2  32355  bnj976  32657  bnj1185  32673  bnj543  32773  bnj571  32786  bnj611  32798  bnj916  32813  bnj1000  32821  bnj1040  32852  iscvm  33121  untuni  33550  dfso3  33566  ralxp3f  33588  dffr5  33627  elima4  33656  ttrcltr  33702  frpoins3xpg  33714  frpoins3xp3g  33715  poxp2  33717  brtxpsd3  34125  brbigcup  34127  fixcnv  34137  ellimits  34139  elfuns  34144  brimage  34155  brcart  34161  brimg  34166  brapply  34167  brcup  34168  brcap  34169  dfrdg4  34180  dfint3  34181  ellines  34381  elicc3  34433  bj-snsetex  35080  bj-snglc  35086  bj-projun  35111  wl-2xor  35581  wl-cases2-dnf  35598  poimirlem27  35731  mblfinlem2  35742  iscrngo2  36082  n0elqs  36388  inxpxrn  36448  eqvrelcoss3  36658  prtlem70  36798  prtlem100  36800  prtlem15  36816  prter2  36822  lcvnbtwn3  36969  ishlat1  37293  ishlat2  37294  hlrelat2  37344  islpln5  37476  islvol5  37520  pclclN  37832  cdleme0nex  38231  isdomn5  40099  aaitgo  40903  isdomn3  40945  imaiun1  41148  relexp0eq  41198  ntrk1k3eqk13  41549  2sbc6g  41922  2sbc5g  41923  2reu7  44490  2reu8  44491  mosssn2  46050  iscnrm3lem3  46117  alsconv  46380