Theorem 3bitr4ri 293

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 267	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 265	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  pm4.78  607  xor  971  cases2  1034  nannan  1588  nic-ax  1735  2sb5  2568  2sb6  2569  2sb5rf  2576  moabs  2627  2mo2  2676  2eu7  2685  2eu8  2686  r3al  3066  r2exlem  3185  risset  3188  r19.35  3210  ralxpxfr2d  3454  reuind  3540  undif3  4019  undif3OLD  4020  unab  4025  inab  4026  n0el  4071  inssdif0  4078  ssundif  4184  ralf0  4210  raldifsnb  4459  pwtp  4571  unipr  4589  uni0b  4603  iinuni  4749  reusv2lem4  5009  pwtr  5058  elxp2OLD  5278  opthprc  5312  xpiundir  5319  xpsspw  5377  relun  5379  inopab  5396  difopab  5397  ralxpf  5412  dmiun  5476  inisegn0  5643  rniun  5689  imaco  5789  mptfnf  6164  fnopabg  6166  dff1o2  6291  brprcneu  6333  idref  6650  imaiun  6654  sorpss  7095  opabex3d  7298  opabex3  7299  ovmptss  7414  fnsuppres  7479  rankc1  8894  aceq1  9101  dfac10  9122  fin41  9429  axgroth6  9813  genpass  9994  infm3  11145  prime  11621  elixx3g  12352  elfz2  12497  elfzuzb  12500  rpnnen2lem12  15124  divalgb  15300  1nprm  15565  maxprmfct  15594  vdwmc  15855  imasleval  16374  issubm  17519  issubg3  17784  efgrelexlemb  18334  ist1-2  21324  unisngl  21503  elflim2  21940  isfcls  21985  istlm  22160  isnlm  22651  ishl2  23337  erclwwlkref  27114  erclwwlknref  27171  0wlk  27239  h1de2ctlem  28694  nonbooli  28790  5oalem7  28799  ho01i  28967  rnbra  29246  cvnbtwn3  29427  chrelat2i  29504  moel  29603  difrab2  29617  uniinn0  29644  disjex  29683  maprnin  29786  ordtconnlem1  30250  esum2dlem  30434  eulerpartgbij  30714  eulerpartlemr  30716  eulerpartlemn  30723  ballotlem2  30830  bnj976  31126  bnj1185  31142  bnj543  31241  bnj571  31254  bnj611  31266  bnj916  31281  bnj1000  31289  bnj1040  31318  iscvm  31519  untuni  31864  dfso3  31879  dffr5  31921  elima4  31955  brtxpsd3  32280  brbigcup  32282  fixcnv  32292  ellimits  32294  elfuns  32299  brimage  32310  brcart  32316  brimg  32321  brapply  32322  brcup  32323  brcap  32324  dfrdg4  32335  dfint3  32336  ellines  32536  elicc3  32588  bj-ssb1  32910  bj-snsetex  33228  bj-snglc  33234  bj-projun  33259  bj-vjust2  33292  wl-cases2-dnf  33577  poimirlem27  33718  mblfinlem2  33729  iscrngo2  34078  ralanid  34304  n0elqs  34391  inxpxrn  34445  prtlem70  34614  prtlem100  34617  prtlem15  34633  prter2  34639  lcvnbtwn3  34787  ishlat1  35111  ishlat2  35112  hlrelat2  35161  islpln5  35293  islvol5  35337  pclclN  35649  cdleme0nex  36049  aaitgo  38203  isdomn3  38253  imaiun1  38414  relexp0eq  38464  ntrk1k3eqk13  38819  2sbc6g  39087  2sbc5g  39088  2reu7  41666  2reu8  41667  alsconv  43018