Theorem 3bitr4ri 307

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biadan  830  pm4.78  947  xor  1030  cases2  1061  4anpull2OLD  1379  nic-ax  1696  nfnbi  1878  2sb6  2122  2sb5  2315  dfsb7  2316  2sb5rf  2506  2sb6rf  2507  eu6lem  2603  eu6  2604  2mo2  2677  2eu7  2687  2eu8  2688  euae  2689  r2exlem  3154  r3al  3203  risset  3240  ralcom4  3291  rexcom4  3292  rabbi  3447  ralxpxfr2d  3608  reuind  3719  dfss2  3925  undif3  4255  unab  4263  inab  4264  n0el  4320  inssdif0  4330  ssundif  4444  ralf0  4454  raldifsnb  4759  pwtp  4862  uni0b  4894  iinuni  5059  inuni  5310  reusv2lem4  5362  pwtr  5423  opthprc  5715  xpiundir  5723  xpsspw  5786  relun  5788  inopab  5806  difopab  5807  ralxpf  5822  dmiun  5893  elidinxp  6036  iresn0n0  6046  inisegn0  6090  rniun  6135  imaco  6241  rnco  6242  rncoOLD  6243  mptfnf  6660  fnopabg  6662  dff1o2  6816  brprcneu  6861  brprcneuALT  6862  idref  7132  imaiun  7233  sorpss  7715  opabex3d  7950  opabex3rd  7951  opabex3  7952  ovmptss  8076  frpoins3xpg  8124  frpoins3xp3g  8125  poxp2  8127  poxp3  8134  fnsuppres  8175  sbthfilem  9170  ttrcltr  9673  rankc1  9830  aceq1  10089  dfac10  10109  fin41  10416  axgroth6  10801  genpass  10982  infm3  12162  prime  12665  elixx3g  13373  elfz2  13530  elfzuzb  13534  rpnnen2lem12  16269  divalgb  16450  1nprm  16725  maxprmfct  16756  vdwmc  17026  imasleval  17583  issubm  18849  issubg3  19199  efgrelexlemb  19808  isdomn5  20783  isdomn2  20784  isdomn3  20787  ist1-2  23461  unisngl  23641  elflim2  24078  isfcls  24123  istlm  24299  isnlm  24789  ishl2  25486  ovoliunlem1  25618  eln0s  28508  zaddscl  28541  readdscl  28646  remulscl  28649  erclwwlkref  30276  erclwwlknref  30325  0wlk  30372  h1de2ctlem  31812  nonbooli  31908  5oalem7  31917  ho01i  32085  rnbra  32364  cvnbtwn3  32545  chrelat2i  32622  difrab2  32750  uniinn0  32803  disjex  32843  maprnin  32984  ordtconnlem1  34226  esum2dlem  34394  eulerpartgbij  34674  eulerpartlemr  34676  eulerpartlemn  34683  ballotlem2  34791  bnj976  35078  bnj1185  35093  bnj543  35193  bnj571  35206  bnj611  35218  bnj916  35233  bnj1000  35241  bnj1040  35272  iscvm  35617  untuni  36067  dfso3  36078  dffr5  36112  elima4  36134  brtxpsd3  36252  brbigcup  36254  fixcnv  36264  ellimits  36266  elfuns  36271  brimage  36282  brcart  36288  brimg  36293  brapply  36294  brcup  36295  brcap  36296  dfrdg4  36309  dfint3  36310  ellines  36510  elicc3  36685  bj-snsetex  37455  bj-snglc  37461  bj-projun  37486  wl-2xor  37984  wl-cases2-dnf  38022  poimirlem27  38153  mblfinlem2  38164  iscrngo2  38503  n0elqs  38838  inxpxrn  38924  eqvrelcoss3  39208  prtlem70  39488  prtlem100  39490  prtlem15  39506  prter2  39512  lcvnbtwn3  39659  ishlat1  39983  ishlat2  39984  hlrelat2  40034  islpln5  40166  islvol5  40210  pclclN  40522  cdleme0nex  40921  eu6w  43265  aaitgo  43746  onmaxnelsup  43807  onsupnmax  43812  nnoeomeqom  43896  imaiun1  44234  relexp0eq  44284  ntrk1k3eqk13  44633  2sbc6g  44984  2sbc5g  44985  2reu7  47704  2reu8  47705  mosssn2  49447  iinxp  49461  ixpv  49520  alsconv  50420