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-mp 5  ax-1 6  ax-2 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  557  orbi1i  758  orass  762  or32  765  dcan  928  dn1dc  955  an6  1316  excxor  1373  trubifal  1411  truxortru  1414  truxorfal  1415  falxortru  1416  falxorfal  1417  alrot4  1479  excom13  1682  sborv  1883  3exdistr  1908  4exdistr  1909  eeeanv  1926  ee4anv  1927  ee8anv  1928  sb3an  1951  sb9  1972  sbnf2  1974  sbco4  2000  2exsb  2002  sb8eu  2032  sb8euh  2042  sbmo  2078  2eu4  2112  2eu7  2113  elsb1  2148  elsb2  2149  r19.26-3  2600  rexcom13  2635  cbvreu  2694  ceqsex2  2770  ceqsex4v  2773  spc3gv  2823  ralrab2  2895  rexrab2  2897  reu2  2918  rmo4  2923  reu8  2926  rmo3f  2927  sbc3an  3016  rmo3  3046  dfss2  3136  ss2rab  3223  rabss  3224  ssrab  3225  dfdif3  3237  undi  3375  undif3ss  3388  difin2  3389  dfnul2  3416  disj  3462  disjsn  3643  uni0c  3820  ssint  3845  iunss  3912  ssextss  4203  eqvinop  4226  opcom  4233  opeqsn  4235  opeqpr  4236  brabsb  4244  opelopabf  4257  opabm  4263  pofun  4295  sotritrieq  4308  uniuni  4434  ordsucim  4482  opeliunxp  4664  xpiundi  4667  brinxp2  4676  ssrel  4697  reliun  4730  cnvuni  4795  dmopab3  4822  opelres  4894  elres  4925  elsnres  4926  intirr  4995  ssrnres  5051  dminxp  5053  dfrel4v  5060  dmsnm  5074  rnco  5115  sb8iota  5165  dffun2  5206  dffun4f  5212  funco  5236  funcnveq  5259  fun11  5263  isarep1  5282  dff1o4  5448  dff1o6  5752  oprabid  5882  mpo2eqb  5959  ralrnmpo  5964  rexrnmpo  5965  opabex3d  6097  opabex3  6098  xporderlem  6207  f1od2  6211  tfr0dm  6298  tfrexlem  6310  frec0g  6373  nnaord  6485  ecid  6572  mptelixpg  6708  elixpsn  6709  mapsnen  6785  xpsnen  6795  xpcomco  6800  xpassen  6804  exmidontriimlem3  7187  nqnq0  7390  opelreal  7776  pitoregt0  7798  elnn0  9124  elxnn0  9187  elxr  9720  xrnepnf  9722  elfzuzb  9962  4fvwrd4  10083  elfzo2  10093  resqrexlemsqa  10975  fisumcom2  11388  modfsummod  11408  fprodcom2fi  11576  nnwosdc  11981  isprm2  12058  isprm4  12060  pythagtriplem2  12207  ntreq0  12885  txbas  13011  metrest  13259