Theorem 3bitri 206

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bibi1i  228  an32  562  orbi1i  764  orass  768  or32  771  dn1dc  962  an6  1332  excxor  1389  trubifal  1427  truxortru  1430  truxorfal  1431  falxortru  1432  falxorfal  1433  alrot4  1497  excom13  1700  sborv  1902  3exdistr  1927  4exdistr  1928  eeeanv  1949  ee4anv  1950  ee8anv  1951  sb3an  1974  sb9  1995  sbnf2  1997  sbco4  2023  2exsb  2025  sb8eu  2055  sb8euh  2065  sbmo  2101  2eu4  2135  2eu7  2136  elsb1  2171  elsb2  2172  r19.26-3  2624  rexcom13  2660  cbvreu  2724  ceqsex2  2800  ceqsex4v  2803  spc3gv  2853  ralrab2  2925  rexrab2  2927  reu2  2948  rmo4  2953  reu8  2956  rmo3f  2957  sbc3an  3047  rmo3  3077  dfss2  3168  ss2rab  3255  rabss  3256  ssrab  3257  dfdif3  3269  undi  3407  undif3ss  3420  difin2  3421  dfnul2  3448  disj  3495  disjsn  3680  snssb  3751  uni0c  3861  ssint  3886  iunss  3953  ssextss  4249  eqvinop  4272  opcom  4279  opeqsn  4281  opeqpr  4282  brabsb  4291  opelopabf  4305  opabm  4311  pofun  4343  sotritrieq  4356  uniuni  4482  ordsucim  4532  opeliunxp  4714  xpiundi  4717  brinxp2  4726  ssrel  4747  reliun  4780  cnvuni  4848  dmopab3  4875  opelres  4947  elres  4978  elsnres  4979  intirr  5052  ssrnres  5108  dminxp  5110  dfrel4v  5117  dmsnm  5131  rnco  5172  sb8iota  5222  dffun2  5264  dffun4f  5270  funco  5294  funcnveq  5317  fun11  5321  isarep1  5340  dff1o4  5508  dff1o6  5819  oprabid  5950  mpo2eqb  6028  ralrnmpo  6033  rexrnmpo  6034  opabex3d  6173  opabex3  6174  xporderlem  6284  f1od2  6288  tfr0dm  6375  tfrexlem  6387  frec0g  6450  nnaord  6562  ecid  6652  mptelixpg  6788  elixpsn  6789  mapsnen  6865  xpsnen  6875  xpcomco  6880  xpassen  6884  exmidontriimlem3  7283  nqnq0  7501  opelreal  7887  pitoregt0  7909  elnn0  9242  elxnn0  9305  elxr  9842  xrnepnf  9844  elfzuzb  10085  4fvwrd4  10206  elfzo2  10216  resqrexlemsqa  11168  fisumcom2  11581  modfsummod  11601  fprodcom2fi  11769  nnwosdc  12176  isprm2  12255  isprm4  12257  pythagtriplem2  12404  4sqlem12  12540  isnsg2  13273  isnsg4  13282  dfrhm2  13650  cnfldui  14077  ntreq0  14300  txbas  14426  metrest  14674