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 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  816  pm4.78  932  xor  1012  cases2  1045  nic-ax  1676  nfnbi  1858  2sb6  2090  2sb5  2273  dfsb7  2277  2sb5rf  2473  2sb6rf  2474  eu6lem  2574  eu6  2575  2mo2  2650  2eu7  2660  2eu8  2661  euae  2662  r3al  3120  ralcom4  3165  risset  3195  r2exlem  3232  rexcom4  3234  moelOLD  3360  ralxpxfr2d  3577  reuind  3689  undif3  4225  unab  4233  inab  4234  n0el  4296  inssdif0  4304  ab0  4309  ssundif  4419  ralf0OLD  4449  raldifsnb  4730  pwtp  4835  uniprOLD  4859  uni0b  4868  iinuni  5028  reusv2lem4  5325  pwtr  5369  opthprc  5652  xpiundir  5659  xpsspw  5721  relun  5723  inopab  5741  difopab  5742  difopabOLD  5743  ralxpf  5758  dmiun  5825  elidinxp  5954  iresn0n0  5966  inisegn0  6009  rniun  6056  imaco  6159  rnco  6160  mptfnf  6577  fnopabg  6579  dff1o2  6730  brprcneu  6773  brprcneuALT  6774  idref  7027  imaiun  7127  sorpss  7590  opabex3d  7817  opabex3rd  7818  opabex3  7819  ovmptss  7942  fnsuppres  8016  sbthfilem  8993  ttrcltr  9483  rankc1  9637  aceq1  9882  dfac10  9902  fin41  10209  axgroth6  10593  genpass  10774  infm3  11943  prime  12410  elixx3g  13101  elfz2  13255  elfzuzb  13259  rpnnen2lem12  15943  divalgb  16122  1nprm  16393  maxprmfct  16423  vdwmc  16688  imasleval  17261  issubm  18451  issubg3  18782  efgrelexlemb  19365  ist1-2  22507  unisngl  22687  elflim2  23124  isfcls  23169  istlm  23345  isnlm  23848  ishl2  24543  ovoliunlem1  24675  erclwwlkref  28393  erclwwlknref  28442  0wlk  28489  h1de2ctlem  29926  nonbooli  30022  5oalem7  30031  ho01i  30199  rnbra  30478  cvnbtwn3  30659  chrelat2i  30736  nelbOLDOLD  30826  difrab2  30854  uniinn0  30899  disjex  30940  maprnin  31075  ordtconnlem1  31883  esum2dlem  32069  eulerpartgbij  32348  eulerpartlemr  32350  eulerpartlemn  32357  ballotlem2  32464  bnj976  32766  bnj1185  32782  bnj543  32882  bnj571  32895  bnj611  32907  bnj916  32922  bnj1000  32930  bnj1040  32961  iscvm  33230  untuni  33659  dfso3  33673  ralxp3f  33694  dffr5  33730  elima4  33759  frpoins3xpg  33796  frpoins3xp3g  33797  poxp2  33799  brtxpsd3  34207  brbigcup  34209  fixcnv  34219  ellimits  34221  elfuns  34226  brimage  34237  brcart  34243  brimg  34248  brapply  34249  brcup  34250  brcap  34251  dfrdg4  34262  dfint3  34263  ellines  34463  elicc3  34515  bj-snsetex  35162  bj-snglc  35168  bj-projun  35193  wl-2xor  35663  wl-cases2-dnf  35680  poimirlem27  35813  mblfinlem2  35824  iscrngo2  36164  n0elqs  36468  inxpxrn  36528  eqvrelcoss3  36738  prtlem70  36878  prtlem100  36880  prtlem15  36896  prter2  36902  lcvnbtwn3  37049  ishlat1  37373  ishlat2  37374  hlrelat2  37424  islpln5  37556  islvol5  37600  pclclN  37912  cdleme0nex  38311  isdomn5  40178  aaitgo  40994  isdomn3  41036  imaiun1  41266  relexp0eq  41316  ntrk1k3eqk13  41667  2sbc6g  42040  2sbc5g  42041  2reu7  44614  2reu8  44615  mosssn2  46173  iscnrm3lem3  46240  alsconv  46505