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  1939  3exdistr  1964  4exdistr  1965  eeeanv  1986  ee4anv  1987  ee8anv  1988  sb3an  2011  sb9  2032  sbnf2  2034  sbco4  2060  2exsb  2062  sb8eu  2092  sb8euh  2102  sbmo  2139  2eu4  2173  2eu7  2174  elsb1  2209  elsb2  2210  r19.26-3  2664  rexcom13  2700  cbvreu  2766  ceqsex2  2845  ceqsex4v  2848  spc3gv  2900  ralrab2  2972  rexrab2  2974  reu2  2995  rmo4  3000  reu8  3003  rmo3f  3004  sbc3an  3094  reu8nf  3114  rmo3  3125  ssalel  3216  ss2rab  3304  rabss  3305  ssrab  3306  dfdif3  3319  undi  3457  undif3ss  3470  difin2  3471  dfnul2  3498  disj  3545  disjsn  3735  snssb  3811  uni0c  3924  ssint  3949  iunss  4016  ssextss  4318  eqvinop  4341  opcom  4349  opeqsn  4351  opeqpr  4352  brabsb  4361  opelopabf  4375  opabm  4381  pofun  4415  sotritrieq  4428  uniuni  4554  ordsucim  4604  opeliunxp  4787  xpiundi  4790  brinxp2  4799  ssrel  4820  reliun  4854  cnvuni  4922  dmopab3  4950  opelres  5024  elres  5055  elsnres  5056  intirr  5130  ssrnres  5186  dminxp  5188  dfrel4v  5195  dmsnm  5209  rnco  5250  sb8iota  5301  dffun2  5343  dffun4f  5349  funco  5373  funcnveq  5400  fun11  5404  isarep1  5423  dff1o4  5600  dff1o6  5927  oprabid  6060  mpo2eqb  6141  ralrnmpo  6146  rexrnmpo  6147  opabex3d  6292  opabex3  6293  xporderlem  6405  f1od2  6409  tfr0dm  6531  tfrexlem  6543  frec0g  6606  nnaord  6720  ecid  6810  mptelixpg  6946  elixpsn  6947  mapsnen  7029  xpsnen  7048  xpcomco  7053  xpassen  7057  exmidontriimlem3  7481  nqnq0  7704  opelreal  8090  pitoregt0  8112  elnn0  9447  elxnn0  9510  elxr  10054  xrnepnf  10056  elfzuzb  10297  4fvwrd4  10418  elfzo2  10428  swrdnd  11287  resqrexlemsqa  11645  fisumcom2  12060  modfsummod  12080  fprodcom2fi  12248  nnwosdc  12671  isprm2  12750  isprm4  12752  pythagtriplem2  12900  4sqlem12  13036  isnsg2  13851  isnsg4  13860  dfrhm2  14230  cnfldui  14665  ntreq0  14923  txbas  15049  metrest  15297  2lgslem4  15902  umgr2edg1  16130  isclwwlk  16315  isclwwlknx  16337  clwwlkn1  16339  clwwlkn2  16342  clwwlknonel  16353  iseupthf1o  16369