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  1673  nfnbi  1855  2sb6  2087  2sb5  2278  dfsb7  2279  2sb5rf  2471  2sb6rf  2472  eu6lem  2567  eu6  2568  2mo2  2641  2eu7  2652  2eu8  2653  euae  2654  r2exlem  3123  r3al  3176  risset  3213  ralcom4  3264  rexcom4  3265  rabbi  3439  ralxpxfr2d  3615  reuind  3727  dfss2  3935  undif3  4266  unab  4274  inab  4275  n0el  4330  inssdif0  4340  ssundif  4454  raldifsnb  4763  pwtp  4869  uni0b  4900  iinuni  5065  inuni  5308  reusv2lem4  5359  pwtr  5415  opthprc  5705  xpiundir  5713  xpsspw  5775  relun  5777  inopab  5795  difopab  5796  difopabOLD  5797  ralxpf  5813  dmiun  5880  elidinxp  6018  iresn0n0  6028  inisegn0  6072  rniun  6123  imaco  6227  rnco  6228  mptfnf  6656  fnopabg  6658  dff1o2  6808  brprcneu  6851  brprcneuALT  6852  idref  7121  imaiun  7222  sorpss  7707  opabex3d  7947  opabex3rd  7948  opabex3  7949  ovmptss  8075  frpoins3xpg  8122  frpoins3xp3g  8123  poxp2  8125  poxp3  8132  fnsuppres  8173  sbthfilem  9168  ttrcltr  9676  rankc1  9830  aceq1  10077  dfac10  10098  fin41  10404  axgroth6  10788  genpass  10969  infm3  12149  prime  12622  elixx3g  13326  elfz2  13482  elfzuzb  13486  rpnnen2lem12  16200  divalgb  16381  1nprm  16656  maxprmfct  16686  vdwmc  16956  imasleval  17511  issubm  18737  issubg3  19083  efgrelexlemb  19687  isdomn5  20626  isdomn2  20627  isdomn3  20631  ist1-2  23241  unisngl  23421  elflim2  23858  isfcls  23903  istlm  24079  isnlm  24570  ishl2  25277  ovoliunlem1  25410  eln0s  28258  zaddscl  28289  readdscl  28357  remulscl  28360  erclwwlkref  29956  erclwwlknref  30005  0wlk  30052  h1de2ctlem  31491  nonbooli  31587  5oalem7  31596  ho01i  31764  rnbra  32043  cvnbtwn3  32224  chrelat2i  32301  difrab2  32434  uniinn0  32486  disjex  32528  maprnin  32661  ordtconnlem1  33921  esum2dlem  34089  eulerpartgbij  34370  eulerpartlemr  34372  eulerpartlemn  34379  ballotlem2  34487  bnj976  34774  bnj1185  34790  bnj543  34890  bnj571  34903  bnj611  34915  bnj916  34930  bnj1000  34938  bnj1040  34969  iscvm  35253  untuni  35703  dfso3  35714  dffr5  35748  elima4  35770  brtxpsd3  35891  brbigcup  35893  fixcnv  35903  ellimits  35905  elfuns  35910  brimage  35921  brcart  35927  brimg  35932  brapply  35933  brcup  35934  brcap  35935  dfrdg4  35946  dfint3  35947  ellines  36147  elicc3  36312  bj-snsetex  36958  bj-snglc  36964  bj-projun  36989  wl-2xor  37478  wl-cases2-dnf  37507  poimirlem27  37648  mblfinlem2  37659  iscrngo2  37998  n0elqs  38321  inxpxrn  38388  eqvrelcoss3  38616  prtlem70  38857  prtlem100  38859  prtlem15  38875  prter2  38881  lcvnbtwn3  39028  ishlat1  39352  ishlat2  39353  hlrelat2  39404  islpln5  39536  islvol5  39580  pclclN  39892  cdleme0nex  40291  eu6w  42671  aaitgo  43158  onmaxnelsup  43219  onsupnmax  43224  nnoeomeqom  43308  imaiun1  43647  relexp0eq  43697  ntrk1k3eqk13  44046  2sbc6g  44411  2sbc5g  44412  2reu7  47116  2reu8  47117  mosssn2  48809  iinxp  48823  ixpv  48882  alsconv  49783