Theorem 3bitr4ri 305

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  biadan  824  pm4.78  940  xor  1022  cases2  1053  4anpull2  1368  nic-ax  1680  nfnbi  1862  2sb6  2097  2sb5  2289  dfsb7  2290  2sb5rf  2480  2sb6rf  2481  eu6lem  2577  eu6  2578  2mo2  2651  2eu7  2662  2eu8  2663  euae  2664  r2exlem  3129  r3al  3178  risset  3215  ralcom4  3266  rexcom4  3267  rabbi  3422  ralxpxfr2d  3591  reuind  3701  dfss2  3908  undif3  4235  unab  4243  inab  4244  n0el  4299  inssdif0  4309  ssundif  4422  ralf0  4432  raldifsnb  4736  pwtp  4840  uni0b  4871  iinuni  5034  inuni  5285  reusv2lem4  5337  pwtr  5398  opthprc  5689  xpiundir  5697  xpsspw  5759  relun  5761  inopab  5779  difopab  5780  ralxpf  5795  dmiun  5862  elidinxp  6003  iresn0n0  6013  inisegn0  6057  rniun  6105  imaco  6209  rnco  6210  rncoOLD  6211  mptfnf  6627  fnopabg  6629  dff1o2  6779  brprcneu  6824  brprcneuALT  6825  idref  7095  imaiun  7196  sorpss  7678  opabex3d  7914  opabex3rd  7915  opabex3  7916  ovmptss  8039  frpoins3xpg  8087  frpoins3xp3g  8088  poxp2  8090  poxp3  8097  fnsuppres  8138  sbthfilem  9129  ttrcltr  9635  rankc1  9792  aceq1  10037  dfac10  10058  fin41  10364  axgroth6  10749  genpass  10930  infm3  12113  prime  12608  elixx3g  13309  elfz2  13466  elfzuzb  13470  rpnnen2lem12  16190  divalgb  16371  1nprm  16646  maxprmfct  16677  vdwmc  16947  imasleval  17503  issubm  18769  issubg3  19118  efgrelexlemb  19723  isdomn5  20689  isdomn2  20690  isdomn3  20694  ist1-2  23337  unisngl  23517  elflim2  23954  isfcls  23999  istlm  24175  isnlm  24665  ishl2  25362  ovoliunlem1  25494  eln0s  28378  zaddscl  28411  readdscl  28516  remulscl  28519  erclwwlkref  30115  erclwwlknref  30164  0wlk  30211  h1de2ctlem  31651  nonbooli  31747  5oalem7  31756  ho01i  31924  rnbra  32203  cvnbtwn3  32384  chrelat2i  32461  difrab2  32592  uniinn0  32646  disjex  32688  maprnin  32830  ordtconnlem1  34115  esum2dlem  34283  eulerpartgbij  34563  eulerpartlemr  34565  eulerpartlemn  34572  ballotlem2  34680  bnj976  34967  bnj1185  34982  bnj543  35082  bnj571  35095  bnj611  35107  bnj916  35122  bnj1000  35130  bnj1040  35161  iscvm  35494  untuni  35944  dfso3  35955  dffr5  35989  elima4  36011  brtxpsd3  36129  brbigcup  36131  fixcnv  36141  ellimits  36143  elfuns  36148  brimage  36159  brcart  36165  brimg  36170  brapply  36171  brcup  36172  brcap  36173  dfrdg4  36186  dfint3  36187  ellines  36387  elicc3  36552  bj-snsetex  37323  bj-snglc  37329  bj-projun  37354  wl-2xor  37852  wl-cases2-dnf  37890  poimirlem27  38021  mblfinlem2  38032  iscrngo2  38371  n0elqs  38706  inxpxrn  38792  eqvrelcoss3  39076  prtlem70  39356  prtlem100  39358  prtlem15  39374  prter2  39380  lcvnbtwn3  39527  ishlat1  39851  ishlat2  39852  hlrelat2  39902  islpln5  40034  islvol5  40078  pclclN  40390  cdleme0nex  40789  eu6w  43133  aaitgo  43614  onmaxnelsup  43675  onsupnmax  43680  nnoeomeqom  43764  imaiun1  44102  relexp0eq  44152  ntrk1k3eqk13  44501  2sbc6g  44866  2sbc5g  44867  2reu7  47581  2reu8  47582  mosssn2  49314  iinxp  49328  ixpv  49387  alsconv  50287