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  1032  cases2  1063  4anpull2OLD  1383  nic-ax  1703  nfnbi  1885  2sb6  2120  2sb5  2313  dfsb7  2314  2sb5rf  2504  2sb6rf  2505  eu6lem  2601  eu6  2602  2mo2  2675  2eu7  2685  2eu8  2686  euae  2687  r2exlem  3154  r3al  3203  risset  3240  ralcom4  3291  rexcom4  3292  rabbi  3446  ralxpxfr2d  3606  reuind  3717  dfss2  3924  undif3  4254  unab  4262  inab  4263  n0el  4320  inssdif0OLD  4331  ssundif  4449  ralf0  4459  raldifsnb  4765  pwtp  4868  uni0b  4900  iinuni  5065  inuni  5322  reusv2lem4  5374  pwtr  5435  opthprc  5727  xpiundir  5735  xpsspw  5798  relun  5800  inopab  5818  difopab  5819  ralxpf  5834  dmiun  5905  elidinxp  6048  iresn0n0  6058  inisegn0  6102  rniun  6147  imaco  6254  rnco  6255  rncoOLD  6256  mptfnf  6672  fnopabg  6674  dff1o2  6828  brprcneu  6873  brprcneuALT  6874  idref  7144  imaiun  7245  sorpss  7727  opabex3d  7963  opabex3rd  7964  opabex3  7965  ovmptss  8089  frpoins3xpg  8137  frpoins3xp3g  8138  poxp2  8140  poxp3  8147  fnsuppres  8188  sbthfilem  9183  ttrcltr  9686  rankc1  9843  aceq1  10102  dfac10  10122  fin41  10429  axgroth6  10814  genpass  10995  infm3  12175  prime  12678  elixx3g  13386  elfz2  13543  elfzuzb  13547  rpnnen2lem12  16282  divalgb  16463  1nprm  16738  maxprmfct  16769  vdwmc  17039  imasleval  17596  issubm  18862  issubg3  19212  efgrelexlemb  19821  isdomn5  20796  isdomn2  20797  isdomn3  20800  ist1-2  23485  unisngl  23665  elflim2  24102  isfcls  24147  istlm  24323  isnlm  24813  ishl2  25510  ovoliunlem1  25642  eln0s  28535  zaddscl  28568  readdscl  28673  remulscl  28676  erclwwlkref  30352  erclwwlknref  30401  0wlk  30448  h1de2ctlem  31888  nonbooli  31984  5oalem7  31993  ho01i  32161  rnbra  32440  cvnbtwn3  32621  chrelat2i  32698  difrab2  32825  uniinn0  32878  disjex  32918  maprnin  33057  ordtconnlem1  34295  esum2dlem  34463  eulerpartgbij  34743  eulerpartlemr  34745  eulerpartlemn  34752  ballotlem2  34860  bnj976  35147  bnj1185  35162  bnj543  35262  bnj571  35275  bnj611  35287  bnj916  35302  bnj1000  35310  bnj1040  35341  iscvm  35732  untuni  36182  dfso3  36193  dffr5  36227  elima4  36249  brtxpsd3  36367  brbigcup  36369  fixcnv  36379  ellimits  36381  elfuns  36386  brimage  36397  brcart  36403  brimg  36408  brapply  36409  brcup  36410  brcap  36411  dfrdg4  36424  dfint3  36425  ellines  36625  elicc3  36809  bj-snsetex  37580  bj-snglc  37586  bj-projun  37611  wl-2xor  38110  wl-cases2-dnf  38148  poimirlem27  38279  mblfinlem2  38290  iscrngo2  38629  n0elqs  38962  inxpxrn  39048  eqvrelcoss3  39332  prtlem70  39612  prtlem100  39614  prtlem15  39630  prter2  39636  lcvnbtwn3  39783  ishlat1  40107  ishlat2  40108  hlrelat2  40158  islpln5  40290  islvol5  40334  pclclN  40646  cdleme0nex  41045  eu6w  43391  aaitgo  43872  onmaxnelsup  43933  onsupnmax  43938  nnoeomeqom  44022  imaiun1  44360  relexp0eq  44410  ntrk1k3eqk13  44759  2sbc6g  45108  2sbc5g  45109  2reu7  47831  2reu8  47832  mosssn2  49578  iinxp  49592  ixpv  49651