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  768  orass  772  or32  775  dn1dc  966  an6  1355  excxor  1420  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  alrot4  1532  excom13  1735  sborv  1937  3exdistr  1962  4exdistr  1963  eeeanv  1984  ee4anv  1985  ee8anv  1986  sb3an  2009  sb9  2030  sbnf2  2032  sbco4  2058  2exsb  2060  sb8eu  2090  sb8euh  2100  sbmo  2137  2eu4  2171  2eu7  2172  elsb1  2207  elsb2  2208  r19.26-3  2661  rexcom13  2697  cbvreu  2763  ceqsex2  2841  ceqsex4v  2844  spc3gv  2896  ralrab2  2968  rexrab2  2970  reu2  2991  rmo4  2996  reu8  2999  rmo3f  3000  sbc3an  3090  reu8nf  3110  rmo3  3121  ssalel  3212  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  undi  3452  undif3ss  3465  difin2  3466  dfnul2  3493  disj  3540  disjsn  3728  snssb  3800  uni0c  3913  ssint  3938  iunss  4005  ssextss  4305  eqvinop  4328  opcom  4336  opeqsn  4338  opeqpr  4339  brabsb  4348  opelopabf  4362  opabm  4368  pofun  4400  sotritrieq  4413  uniuni  4539  ordsucim  4589  opeliunxp  4771  xpiundi  4774  brinxp2  4783  ssrel  4804  reliun  4837  cnvuni  4905  dmopab3  4933  opelres  5006  elres  5037  elsnres  5038  intirr  5111  ssrnres  5167  dminxp  5169  dfrel4v  5176  dmsnm  5190  rnco  5231  sb8iota  5282  dffun2  5324  dffun4f  5330  funco  5354  funcnveq  5380  fun11  5384  isarep1  5403  dff1o4  5576  dff1o6  5893  oprabid  6026  mpo2eqb  6105  ralrnmpo  6110  rexrnmpo  6111  opabex3d  6256  opabex3  6257  xporderlem  6367  f1od2  6371  tfr0dm  6458  tfrexlem  6470  frec0g  6533  nnaord  6645  ecid  6735  mptelixpg  6871  elixpsn  6872  mapsnen  6954  xpsnen  6968  xpcomco  6973  xpassen  6977  exmidontriimlem3  7393  nqnq0  7616  opelreal  8002  pitoregt0  8024  elnn0  9359  elxnn0  9422  elxr  9960  xrnepnf  9962  elfzuzb  10203  4fvwrd4  10324  elfzo2  10334  swrdnd  11177  resqrexlemsqa  11521  fisumcom2  11935  modfsummod  11955  fprodcom2fi  12123  nnwosdc  12546  isprm2  12625  isprm4  12627  pythagtriplem2  12775  4sqlem12  12911  isnsg2  13726  isnsg4  13735  dfrhm2  14103  cnfldui  14538  ntreq0  14791  txbas  14917  metrest  15165  2lgslem4  15767  umgr2edg1  15992