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

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1i  228  an32  568  orbi1i  775  orass  779  or32  782  dn1dc  973  an6  1362  excxor  1427  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  alrot4  1539  excom13  1741  sborv  1945  3exdistr  1971  4exdistr  1972  eeeanv  1993  ee4anv  1994  ee8anv  1995  sb3an  2018  sb9  2039  sbnf2  2041  sbco4  2067  2exsb  2069  sb8eu  2099  sb8euh  2109  sbmo  2146  2eu4  2180  2eu7  2181  elsb1  2216  elsb2  2217  r19.26-3  2681  rexcom13  2717  cbvreu  2784  ceqsex2  2863  ceqsex4v  2866  spc3gv  2918  ralrab2  2991  rexrab2  2993  reu2  3014  rmo4  3019  reu8  3022  rmo3f  3023  sbc3an  3113  reu8nf  3133  rmo3  3144  ssalel  3235  ss2rab  3324  rabss  3325  ssrab  3326  dfdif3  3339  undi  3479  undif3ss  3492  difin2  3493  disj  3573  disjsn  3771  snssb  3848  uni0c  3961  ssint  3986  iunss  4053  ssextss  4362  eqvinop  4385  opcom  4393  opeqsn  4395  opeqpr  4396  brabsb  4405  opelopabf  4419  opabm  4425  pofun  4459  sotritrieq  4472  uniuni  4599  ordsucim  4649  opeliunxp  4832  xpiundi  4835  brinxp2  4844  ssrel  4865  reliun  4900  cnvuni  4968  dmopab3  4996  opelres  5070  elres  5101  elsnres  5102  intirr  5177  ssrnres  5233  dminxp  5235  dfrel4v  5242  dmsnm  5256  rnco  5297  sb8iota  5348  dffun2  5390  dffun4f  5396  funco  5420  funcnveq  5447  fun11  5451  isarep1  5470  dff1o4  5650  dff1o6  5985  oprabid  6120  mpo2eqb  6201  ralrnmpo  6206  rexrnmpo  6207  opabex3d  6354  opabex3  6355  xporderlem  6471  f1od2  6475  tfr0dm  6597  tfrexlem  6609  frec0g  6672  nnaord  6786  ecid  6876  mptelixpg  7021  elixpsn  7022  mapsnen  7105  xpsnen  7124  xpcomco  7129  xpassen  7133  exmidontriimlem3  7586  nqnq0  7815  opelreal  8201  pitoregt0  8223  elnn0  9577  elxnn0  9644  elxr  10196  xrnepnf  10198  elfzuzb  10440  4fvwrd4  10565  elfzo2  10575  swrdnd  11454  resqrexlemsqa  11813  fisumcom2  12231  modfsummod  12251  fprodcom2fi  12419  nnwosdc  12842  isprm2  12921  isprm4  12923  pythagtriplem2  13075  4sqlem12  13211  isnsg2  14066  isnsg4  14075  dfrhm2  14571  cnfldui  15034  isassa  15112  ntreq0  15370  txbas  15496  metrest  15744  2lgslem4  16439  umgr2edg1  16667  isclwwlk  16852  isclwwlknx  16874  clwwlkn1  16876  clwwlkn2  16879  clwwlknonel  16890  iseupthf1o  16906  alsanmo  17370  ralsanmo  17371