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  dcan  934  dn1dc  961  an6  1331  excxor  1388  trubifal  1426  truxortru  1429  truxorfal  1430  falxortru  1431  falxorfal  1432  alrot4  1496  excom13  1699  sborv  1901  3exdistr  1926  4exdistr  1927  eeeanv  1944  ee4anv  1945  ee8anv  1946  sb3an  1969  sb9  1990  sbnf2  1992  sbco4  2018  2exsb  2020  sb8eu  2050  sb8euh  2060  sbmo  2096  2eu4  2130  2eu7  2131  elsb1  2166  elsb2  2167  r19.26-3  2619  rexcom13  2655  cbvreu  2715  ceqsex2  2791  ceqsex4v  2794  spc3gv  2844  ralrab2  2916  rexrab2  2918  reu2  2939  rmo4  2944  reu8  2947  rmo3f  2948  sbc3an  3038  rmo3  3068  dfss2  3158  ss2rab  3245  rabss  3246  ssrab  3247  dfdif3  3259  undi  3397  undif3ss  3410  difin2  3411  dfnul2  3438  disj  3485  disjsn  3668  snssb  3739  uni0c  3849  ssint  3874  iunss  3941  ssextss  4234  eqvinop  4257  opcom  4264  opeqsn  4266  opeqpr  4267  brabsb  4275  opelopabf  4288  opabm  4294  pofun  4326  sotritrieq  4339  uniuni  4465  ordsucim  4513  opeliunxp  4695  xpiundi  4698  brinxp2  4707  ssrel  4728  reliun  4761  cnvuni  4827  dmopab3  4854  opelres  4926  elres  4957  elsnres  4958  intirr  5029  ssrnres  5085  dminxp  5087  dfrel4v  5094  dmsnm  5108  rnco  5149  sb8iota  5199  dffun2  5240  dffun4f  5246  funco  5270  funcnveq  5293  fun11  5297  isarep1  5316  dff1o4  5483  dff1o6  5792  oprabid  5922  mpo2eqb  6000  ralrnmpo  6005  rexrnmpo  6006  opabex3d  6139  opabex3  6140  xporderlem  6249  f1od2  6253  tfr0dm  6340  tfrexlem  6352  frec0g  6415  nnaord  6527  ecid  6615  mptelixpg  6751  elixpsn  6752  mapsnen  6828  xpsnen  6838  xpcomco  6843  xpassen  6847  exmidontriimlem3  7239  nqnq0  7457  opelreal  7843  pitoregt0  7865  elnn0  9195  elxnn0  9258  elxr  9793  xrnepnf  9795  elfzuzb  10036  4fvwrd4  10157  elfzo2  10167  resqrexlemsqa  11050  fisumcom2  11463  modfsummod  11483  fprodcom2fi  11651  nnwosdc  12057  isprm2  12134  isprm4  12136  pythagtriplem2  12283  isnsg2  13107  isnsg4  13116  dfrhm2  13464  ntreq0  14015  txbas  14141  metrest  14389