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 205

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 206

This theorem is referenced by:  biadan  818  pm4.78  934  xor  1014  cases2  1047  nic-ax  1676  nfnbi  1858  2sb6  2090  2sb5  2272  dfsb7  2276  2sb5rf  2472  2sb6rf  2473  eu6lem  2568  eu6  2569  2mo2  2644  2eu7  2654  2eu8  2655  euae  2656  r2exlem  3144  r3al  3197  risset  3231  ralcom4  3284  rexcom4  3286  moelOLD  3402  rabbi  3463  ralxpxfr2d  3635  reuind  3750  undif3  4291  unab  4299  inab  4300  n0el  4362  inssdif0  4370  ssundif  4488  ralf0OLD  4518  raldifsnb  4800  pwtp  4904  uniprOLD  4928  uni0b  4938  iinuni  5102  reusv2lem4  5400  pwtr  5453  opthprc  5741  xpiundir  5748  xpsspw  5810  relun  5812  inopab  5830  difopab  5831  difopabOLD  5832  ralxpf  5847  dmiun  5914  elidinxp  6044  iresn0n0  6054  inisegn0  6098  rniun  6148  imaco  6251  rnco  6252  mptfnf  6686  fnopabg  6688  dff1o2  6839  brprcneu  6882  brprcneuALT  6883  idref  7144  imaiun  7244  sorpss  7718  opabex3d  7952  opabex3rd  7953  opabex3  7954  ovmptss  8079  frpoins3xpg  8126  frpoins3xp3g  8127  poxp2  8129  poxp3  8136  fnsuppres  8176  sbthfilem  9201  ttrcltr  9711  rankc1  9865  aceq1  10112  dfac10  10132  fin41  10439  axgroth6  10823  genpass  11004  infm3  12173  prime  12643  elixx3g  13337  elfz2  13491  elfzuzb  13495  rpnnen2lem12  16168  divalgb  16347  1nprm  16616  maxprmfct  16646  vdwmc  16911  imasleval  17487  issubm  18684  issubg3  19024  efgrelexlemb  19618  isdomn5  20917  ist1-2  22851  unisngl  23031  elflim2  23468  isfcls  23513  istlm  23689  isnlm  24192  ishl2  24887  ovoliunlem1  25019  erclwwlkref  29273  erclwwlknref  29322  0wlk  29369  h1de2ctlem  30808  nonbooli  30904  5oalem7  30913  ho01i  31081  rnbra  31360  cvnbtwn3  31541  chrelat2i  31618  difrab2  31738  uniinn0  31782  disjex  31823  maprnin  31956  ordtconnlem1  32904  esum2dlem  33090  eulerpartgbij  33371  eulerpartlemr  33373  eulerpartlemn  33380  ballotlem2  33487  bnj976  33788  bnj1185  33804  bnj543  33904  bnj571  33917  bnj611  33929  bnj916  33944  bnj1000  33952  bnj1040  33983  iscvm  34250  untuni  34678  dfso3  34689  dffr5  34724  elima4  34747  brtxpsd3  34868  brbigcup  34870  fixcnv  34880  ellimits  34882  elfuns  34887  brimage  34898  brcart  34904  brimg  34909  brapply  34910  brcup  34911  brcap  34912  dfrdg4  34923  dfint3  34924  ellines  35124  elicc3  35202  bj-snsetex  35844  bj-snglc  35850  bj-projun  35875  wl-2xor  36364  wl-cases2-dnf  36381  poimirlem27  36515  mblfinlem2  36526  iscrngo2  36865  n0elqs  37195  inxpxrn  37265  eqvrelcoss3  37488  prtlem70  37727  prtlem100  37729  prtlem15  37745  prter2  37751  lcvnbtwn3  37898  ishlat1  38222  ishlat2  38223  hlrelat2  38274  islpln5  38406  islvol5  38450  pclclN  38762  cdleme0nex  39161  aaitgo  41904  isdomn3  41946  onmaxnelsup  41972  onsupnmax  41977  nnoeomeqom  42062  imaiun1  42402  relexp0eq  42452  ntrk1k3eqk13  42801  2sbc6g  43174  2sbc5g  43175  2reu7  45819  2reu8  45820  mosssn2  47501  iscnrm3lem3  47568  alsconv  47837