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 ⊢ (𝜃 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biadan  831  pm4.78  948  xor  1032  cases2  1063  4anpull2OLD  1383  nic-ax  1705  nfnbi  1887  2sb6  2122  2sb5  2311  dfsb7  2312  2sb5rf  2501  2sb6rf  2502  eu6lem  2598  eu6  2599  2mo2  2672  2eu7  2682  2eu8  2683  euae  2684  r2exlem  3151  r3al  3200  risset  3237  ralcom4  3288  rexcom4  3289  rabbi  3441  ralxpxfr2d  3599  reuind  3710  dfss2  4094  undif3  4245  unab  4253  inab  4254  n0el  4311  inssdif0OLD  4322  ssundif  4442  ralf0  4452  raldifsnb  4755  pwtp  4828  uni0b  4893  iinuni  5057  inuni  5310  reusv2lem4  5362  pwtr  5419  opthprc  5714  xpiundir  5722  xpsspw  5786  relun  5788  inopab  5806  difopab  5807  ralxpf  5823  dmiun  5894  elidinxp  6035  iresn0n0  6045  inisegn0  6095  rniun  6138  imaco  6252  rnco  6253  rncoOLD  6254  mptfnf  6675  fnopabg  6677  dff1o2  6831  brprcneu  6876  brprcneuALT  6877  idref  7150  imaiun  7250  sorpss  7745  opabex3d  7978  opabex3rd  7979  opabex3  7980  ovmptssOLD  8106  frpoins3xpg  8160  frpoins3xp3g  8161  poxp2  8163  poxp3  8170  fnsuppres  8212  sbthfilem  9217  ttrcltr  9721  rankc1  9891  aceq1  10200  dfac10  10220  fin41  10526  axgroth6  10917  genpass  11098  infm3  12280  prime  12784  elixx3g  13493  elfz2  13650  elfzuzb  13654  rpnnen2lem12  16399  divalgb  16580  1nprm  16860  maxprmfct  16891  vdwmc  17162  imasleval  17719  issubm  19004  issubg3  19361  efgrelexlemb  19970  isdomn5  20968  isdomn2  20969  isdomn3  20972  ist1-2  23671  unisngl  23852  elflim2  24289  isfcls  24334  istlm  24510  isnlm  25000  ishl2  25697  ovoliunlem1  25829  eln0s  28753  zaddscl  28786  readdscl  28891  remulscl  28894  erclwwlkref  30617  erclwwlknref  30666  0wlk  30713  h1de2ctlem  32163  nonbooli  32259  5oalem7  32268  ho01i  32436  rnbra  32715  cvnbtwn3  32896  chrelat2i  32973  difrab2  33142  uniinn0  33195  disjex  33234  maprnin  33370  ordtconnlem1  34603  esum2dlem  34771  eulerpartgbij  35051  eulerpartlemr  35053  eulerpartlemn  35060  ballotlem2  35168  bnj976  35455  bnj1185  35470  bnj543  35570  bnj571  35583  bnj611  35595  bnj916  35610  bnj1000  35618  bnj1040  35649  rankse  35794  onprcf1acwevdlem1  35965  iscvm  36111  untuni  36567  dfso3  36578  dffr5  36612  elima4  36633  brtxpsd3  36751  brbigcup  36753  fixcnv  36763  ellimits  36765  elfuns  36770  brimage  36781  brcart  36787  brimg  36792  brapply  36793  brcup  36794  brcap  36795  dfrdg4  36808  dfint3  36809  dffr7  36813  ellines  37010  elicc3  37198  bj-snsetex  37969  bj-snglc  37975  bj-projun  38000  wl-2xor  38500  wl-cases2-dnf  38538  poimirlem27  38659  mblfinlem2  38670  iscrngo2  39025  n0elqs  39358  inxpxrn  39444  eqvrelcoss3  39728  prtlem70  40008  prtlem100  40010  prtlem15  40026  prter2  40032  lcvnbtwn3  40179  ishlat1  40503  ishlat2  40504  hlrelat2  40554  islpln5  40686  islvol5  40730  pclclN  41042  cdleme0nex  41441  eu6w  43781  aaitgo  44258  onmaxnelsup  44319  onsupnmax  44324  nnoeomeqom  44408  imaiun1  44745  relexp0eq  44795  ntrk1k3eqk13  45144  2sbc6g  45493  2sbc5g  45494  2reu7  48275  2reu8  48276  rrx2xpref1o  49925  mosssn2  50022  iinxp  50036  ixpv  50097