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  1674  nfnbi  1856  2sb6  2091  2sb5  2282  dfsb7  2283  2sb5rf  2474  2sb6rf  2475  eu6lem  2570  eu6  2571  2mo2  2644  2eu7  2655  2eu8  2656  euae  2657  r2exlem  3122  r3al  3171  risset  3208  ralcom4  3259  rexcom4  3260  rabbi  3426  ralxpxfr2d  3597  reuind  3708  dfss2  3916  undif3  4249  unab  4257  inab  4258  n0el  4313  inssdif0  4323  ssundif  4437  ralf0  4447  raldifsnb  4749  pwtp  4855  uni0b  4886  iinuni  5050  inuni  5292  reusv2lem4  5343  pwtr  5397  opthprc  5685  xpiundir  5693  xpsspw  5755  relun  5757  inopab  5775  difopab  5776  ralxpf  5792  dmiun  5859  elidinxp  5999  iresn0n0  6009  inisegn0  6053  rniun  6101  imaco  6205  rnco  6206  rncoOLD  6207  mptfnf  6623  fnopabg  6625  dff1o2  6775  brprcneu  6820  brprcneuALT  6821  idref  7087  imaiun  7187  sorpss  7669  opabex3d  7905  opabex3rd  7906  opabex3  7907  ovmptss  8031  frpoins3xpg  8078  frpoins3xp3g  8079  poxp2  8081  poxp3  8088  fnsuppres  8129  sbthfilem  9116  ttrcltr  9615  rankc1  9772  aceq1  10017  dfac10  10038  fin41  10344  axgroth6  10728  genpass  10909  infm3  12090  prime  12562  elixx3g  13262  elfz2  13418  elfzuzb  13422  rpnnen2lem12  16138  divalgb  16319  1nprm  16594  maxprmfct  16624  vdwmc  16894  imasleval  17449  issubm  18715  issubg3  19061  efgrelexlemb  19666  isdomn5  20629  isdomn2  20630  isdomn3  20634  ist1-2  23265  unisngl  23445  elflim2  23882  isfcls  23927  istlm  24103  isnlm  24593  ishl2  25300  ovoliunlem1  25433  eln0s  28290  zaddscl  28321  readdscl  28404  remulscl  28407  erclwwlkref  30004  erclwwlknref  30053  0wlk  30100  h1de2ctlem  31539  nonbooli  31635  5oalem7  31644  ho01i  31812  rnbra  32091  cvnbtwn3  32272  chrelat2i  32349  difrab2  32481  uniinn0  32534  disjex  32576  maprnin  32720  ordtconnlem1  33960  esum2dlem  34128  eulerpartgbij  34408  eulerpartlemr  34410  eulerpartlemn  34417  ballotlem2  34525  bnj976  34812  bnj1185  34828  bnj543  34928  bnj571  34941  bnj611  34953  bnj916  34968  bnj1000  34976  bnj1040  35007  iscvm  35326  untuni  35776  dfso3  35787  dffr5  35821  elima4  35843  brtxpsd3  35961  brbigcup  35963  fixcnv  35973  ellimits  35975  elfuns  35980  brimage  35991  brcart  35997  brimg  36002  brapply  36003  brcup  36004  brcap  36005  dfrdg4  36018  dfint3  36019  ellines  36219  elicc3  36384  bj-snsetex  37030  bj-snglc  37036  bj-projun  37061  wl-2xor  37550  wl-cases2-dnf  37579  poimirlem27  37710  mblfinlem2  37721  iscrngo2  38060  n0elqs  38387  inxpxrn  38465  eqvrelcoss3  38737  prtlem70  38979  prtlem100  38981  prtlem15  38997  prter2  39003  lcvnbtwn3  39150  ishlat1  39474  ishlat2  39475  hlrelat2  39525  islpln5  39657  islvol5  39701  pclclN  40013  cdleme0nex  40412  eu6w  42797  aaitgo  43282  onmaxnelsup  43343  onsupnmax  43348  nnoeomeqom  43432  imaiun1  43771  relexp0eq  43821  ntrk1k3eqk13  44170  2sbc6g  44535  2sbc5g  44536  2reu7  47238  2reu8  47239  mosssn2  48944  iinxp  48958  ixpv  49017  alsconv  49918