Theorem 3bitri 205

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 183	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 183	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1i  227  an32  534  orbi1i  735  orass  739  or32  742  dcan  901  dn1dc  927  an6  1282  excxor  1339  trubifal  1377  truxortru  1380  truxorfal  1381  falxortru  1382  falxorfal  1383  alrot4  1445  excom13  1650  sborv  1844  3exdistr  1867  4exdistr  1868  eeeanv  1883  ee4anv  1884  ee8anv  1885  sb3an  1907  elsb3  1927  elsb4  1928  sb9  1930  sbnf2  1932  sbco4  1958  2exsb  1960  sb8eu  1988  sb8euh  1998  sbmo  2034  2eu4  2068  2eu7  2069  r19.26-3  2536  rexcom13  2570  cbvreu  2626  ceqsex2  2697  ceqsex4v  2700  spc3gv  2749  ralrab2  2818  rexrab2  2820  reu2  2841  rmo4  2846  reu8  2849  rmo3f  2850  sbc3an  2938  rmo3  2968  dfss2  3052  ss2rab  3139  rabss  3140  ssrab  3141  dfdif3  3152  undi  3290  undif3ss  3303  difin2  3304  dfnul2  3331  disj  3377  disjsn  3551  uni0c  3728  ssint  3753  iunss  3820  ssextss  4102  eqvinop  4125  opcom  4132  opeqsn  4134  opeqpr  4135  brabsb  4143  opelopabf  4156  opabm  4162  pofun  4194  sotritrieq  4207  uniuni  4332  ordsucim  4376  opeliunxp  4554  xpiundi  4557  brinxp2  4566  ssrel  4587  reliun  4620  cnvuni  4685  dmopab3  4712  opelres  4782  elres  4813  elsnres  4814  intirr  4883  ssrnres  4939  dminxp  4941  dfrel4v  4948  dmsnm  4962  rnco  5003  sb8iota  5053  dffun2  5091  dffun4f  5097  funco  5121  funcnveq  5144  fun11  5148  isarep1  5167  dff1o4  5331  dff1o6  5631  oprabid  5757  mpo2eqb  5834  ralrnmpo  5839  rexrnmpo  5840  opabex3d  5973  opabex3  5974  xporderlem  6082  f1od2  6086  tfr0dm  6173  tfrexlem  6185  frec0g  6248  nnaord  6359  ecid  6446  mptelixpg  6582  elixpsn  6583  mapsnen  6659  xpsnen  6668  xpcomco  6673  xpassen  6677  nqnq0  7197  opelreal  7562  pitoregt0  7584  elnn0  8883  elxnn0  8946  elxr  9456  xrnepnf  9458  elfzuzb  9693  4fvwrd4  9810  elfzo2  9820  resqrexlemsqa  10688  fisumcom2  11099  modfsummod  11119  isprm2  11644  isprm4  11646  ntreq0  12144  txbas  12269  metrest  12495