Theorem 3bitr4ri 303

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 277	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 275	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  815  pm4.78  931  xor  1011  cases2  1044  nic-ax  1673  nfnbi  1855  2sb6  2087  2sb5  2269  dfsb7  2273  2sb5rf  2469  2sb6rf  2470  eu6lem  2565  eu6  2566  2mo2  2641  2eu7  2651  2eu8  2652  euae  2653  r2exlem  3141  r3al  3194  risset  3228  ralcom4  3281  rexcom4  3283  moelOLD  3399  rabbi  3460  ralxpxfr2d  3633  reuind  3748  undif3  4289  unab  4297  inab  4298  n0el  4360  inssdif0  4368  ssundif  4486  ralf0OLD  4516  raldifsnb  4798  pwtp  4902  uniprOLD  4926  uni0b  4936  iinuni  5100  reusv2lem4  5398  pwtr  5451  opthprc  5739  xpiundir  5746  xpsspw  5808  relun  5810  inopab  5828  difopab  5829  difopabOLD  5830  ralxpf  5845  dmiun  5912  elidinxp  6042  iresn0n0  6052  inisegn0  6096  rniun  6146  imaco  6249  rnco  6250  mptfnf  6684  fnopabg  6686  dff1o2  6837  brprcneu  6880  brprcneuALT  6881  idref  7145  imaiun  7246  sorpss  7720  opabex3d  7954  opabex3rd  7955  opabex3  7956  ovmptss  8081  frpoins3xpg  8128  frpoins3xp3g  8129  poxp2  8131  poxp3  8138  fnsuppres  8178  sbthfilem  9203  ttrcltr  9713  rankc1  9867  aceq1  10114  dfac10  10134  fin41  10441  axgroth6  10825  genpass  11006  infm3  12177  prime  12647  elixx3g  13341  elfz2  13495  elfzuzb  13499  rpnnen2lem12  16172  divalgb  16351  1nprm  16620  maxprmfct  16650  vdwmc  16915  imasleval  17491  issubm  18720  issubg3  19060  efgrelexlemb  19659  isdomn5  21117  ist1-2  23071  unisngl  23251  elflim2  23688  isfcls  23733  istlm  23909  isnlm  24412  ishl2  25118  ovoliunlem1  25251  erclwwlkref  29540  erclwwlknref  29589  0wlk  29636  h1de2ctlem  31075  nonbooli  31171  5oalem7  31180  ho01i  31348  rnbra  31627  cvnbtwn3  31808  chrelat2i  31885  difrab2  32005  uniinn0  32049  disjex  32090  maprnin  32223  ordtconnlem1  33202  esum2dlem  33388  eulerpartgbij  33669  eulerpartlemr  33671  eulerpartlemn  33678  ballotlem2  33785  bnj976  34086  bnj1185  34102  bnj543  34202  bnj571  34215  bnj611  34227  bnj916  34242  bnj1000  34250  bnj1040  34281  iscvm  34548  untuni  34982  dfso3  34993  dffr5  35028  elima4  35051  brtxpsd3  35172  brbigcup  35174  fixcnv  35184  ellimits  35186  elfuns  35191  brimage  35202  brcart  35208  brimg  35213  brapply  35214  brcup  35215  brcap  35216  dfrdg4  35227  dfint3  35228  ellines  35428  elicc3  35505  bj-snsetex  36147  bj-snglc  36153  bj-projun  36178  wl-2xor  36667  wl-cases2-dnf  36684  poimirlem27  36818  mblfinlem2  36829  iscrngo2  37168  n0elqs  37498  inxpxrn  37568  eqvrelcoss3  37791  prtlem70  38030  prtlem100  38032  prtlem15  38048  prter2  38054  lcvnbtwn3  38201  ishlat1  38525  ishlat2  38526  hlrelat2  38577  islpln5  38709  islvol5  38753  pclclN  39065  cdleme0nex  39464  aaitgo  42206  isdomn3  42248  onmaxnelsup  42274  onsupnmax  42279  nnoeomeqom  42364  imaiun1  42704  relexp0eq  42754  ntrk1k3eqk13  43103  2sbc6g  43476  2sbc5g  43477  2reu7  46117  2reu8  46118  mosssn2  47588  iscnrm3lem3  47655  alsconv  47924