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  564  orbi1i  771  orass  775  or32  778  dn1dc  969  an6  1358  excxor  1423  trubifal  1461  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  alrot4  1535  excom13  1737  sborv  1941  3exdistr  1967  4exdistr  1968  eeeanv  1989  ee4anv  1990  ee8anv  1991  sb3an  2014  sb9  2035  sbnf2  2037  sbco4  2063  2exsb  2065  sb8eu  2095  sb8euh  2105  sbmo  2142  2eu4  2176  2eu7  2177  elsb1  2212  elsb2  2213  r19.26-3  2675  rexcom13  2711  cbvreu  2778  ceqsex2  2857  ceqsex4v  2860  spc3gv  2912  ralrab2  2985  rexrab2  2987  reu2  3008  rmo4  3013  reu8  3016  rmo3f  3017  sbc3an  3107  reu8nf  3127  rmo3  3138  ssalel  3229  ss2rab  3318  rabss  3319  ssrab  3320  dfdif3  3333  undi  3473  undif3ss  3486  difin2  3487  dfnul2  3514  disj  3561  disjsn  3756  snssb  3832  uni0c  3945  ssint  3970  iunss  4037  ssextss  4341  eqvinop  4364  opcom  4372  opeqsn  4374  opeqpr  4375  brabsb  4384  opelopabf  4398  opabm  4404  pofun  4438  sotritrieq  4451  uniuni  4577  ordsucim  4627  opeliunxp  4810  xpiundi  4813  brinxp2  4822  ssrel  4843  reliun  4878  cnvuni  4946  dmopab3  4974  opelres  5048  elres  5079  elsnres  5080  intirr  5154  ssrnres  5210  dminxp  5212  dfrel4v  5219  dmsnm  5233  rnco  5274  sb8iota  5325  dffun2  5367  dffun4f  5373  funco  5397  funcnveq  5424  fun11  5428  isarep1  5447  dff1o4  5627  dff1o6  5955  oprabid  6090  mpo2eqb  6171  ralrnmpo  6176  rexrnmpo  6177  opabex3d  6323  opabex3  6324  xporderlem  6440  f1od2  6444  tfr0dm  6566  tfrexlem  6578  frec0g  6641  nnaord  6755  ecid  6845  mptelixpg  6982  elixpsn  6983  mapsnen  7066  xpsnen  7085  xpcomco  7090  xpassen  7094  exmidontriimlem3  7543  nqnq0  7772  opelreal  8158  pitoregt0  8180  elnn0  9515  elxnn0  9582  elxr  10128  xrnepnf  10130  elfzuzb  10372  4fvwrd4  10496  elfzo2  10506  swrdnd  11376  resqrexlemsqa  11734  fisumcom2  12149  modfsummod  12169  fprodcom2fi  12337  nnwosdc  12760  isprm2  12839  isprm4  12841  pythagtriplem2  12989  4sqlem12  13125  isnsg2  14004  isnsg4  14013  dfrhm2  14384  cnfldui  14849  ntreq0  15109  txbas  15235  metrest  15483  2lgslem4  16088  umgr2edg1  16316  isclwwlk  16501  isclwwlknx  16523  clwwlkn1  16525  clwwlkn2  16528  clwwlknonel  16539  iseupthf1o  16555