Theorem 3bitri 204

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitri.1	⊢ (𝜑 ↔ 𝜓)
3bitri.2	⊢ (𝜓 ↔ 𝜒)
3bitri.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitri	⊢ (𝜑 ↔ 𝜃)

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		3bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3		3bitri.3	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	2, 3	bitri 182	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 182	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi1i  226  an32  526  orbi1i  712  orass  716  or32  719  dcan  875  dn1dc  901  an6  1252  excxor  1309  trubifal  1347  truxortru  1350  truxorfal  1351  falxortru  1352  falxorfal  1353  alrot4  1415  excom13  1619  sborv  1811  3exdistr  1833  4exdistr  1834  eeeanv  1849  ee4anv  1850  ee8anv  1851  sb3an  1873  elsb3  1893  elsb4  1894  sb9  1896  sbnf2  1898  sbco4  1924  2exsb  1926  sb8eu  1954  sb8euh  1964  sbmo  2000  2eu4  2034  2eu7  2035  r19.26-3  2487  rexcom13  2519  cbvreu  2575  ceqsex2  2639  ceqsex4v  2642  spc3gv  2690  ralrab2  2757  rexrab2  2759  reu2  2780  rmo4  2785  reu8  2788  sbc3an  2875  rmo3  2905  dfss2  2988  ss2rab  3070  rabss  3071  ssrab  3072  undi  3212  undif3ss  3225  difin2  3226  dfnul2  3253  disj  3292  disjsn  3454  uni0c  3627  ssint  3652  iunss  3719  ssextss  3975  eqvinop  3998  opcom  4005  opeqsn  4007  opeqpr  4008  brabsb  4016  opelopabf  4029  opabm  4035  pofun  4067  sotritrieq  4080  uniuni  4201  ordsucim  4244  opeliunxp  4413  xpiundi  4416  brinxp2  4425  ssrel  4446  reliun  4476  cnvuni  4539  dmopab3  4566  opelres  4635  elres  4664  elsnres  4665  intirr  4731  ssrnres  4783  dminxp  4785  dfrel4v  4792  dmsnm  4806  rnco  4847  sb8iota  4894  dffun2  4932  dffun4f  4938  funco  4960  funcnveq  4982  fun11  4986  isarep1  5005  dff1o4  5154  dff1o6  5436  oprabid  5557  mpt22eqb  5630  ralrnmpt2  5635  rexrnmpt2  5636  opabex3d  5768  opabex3  5769  xporderlem  5872  f1od2  5876  tfr0  5960  tfrexlem  5971  frec0g  6006  nnaord  6105  ecid  6192  xpsnen  6318  xpcomco  6323  xpassen  6327  nqnq0  6631  opelreal  6996  pitoregt0  7017  elnn0  8290  elxr  8850  xrnepnf  8854  elfzuzb  9039  4fvwrd4  9150  elfzo2  9160  resqrexlemsqa  9910  isprm2  10499  isprm4  10501