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  1940  3exdistr  1965  4exdistr  1966  eeeanv  1987  ee4anv  1988  ee8anv  1989  sb3an  2012  sb9  2033  sbnf2  2035  sbco4  2061  2exsb  2063  sb8eu  2093  sb8euh  2103  sbmo  2140  2eu4  2174  2eu7  2175  elsb1  2210  elsb2  2211  r19.26-3  2673  rexcom13  2709  cbvreu  2775  ceqsex2  2854  ceqsex4v  2857  spc3gv  2909  ralrab2  2981  rexrab2  2983  reu2  3004  rmo4  3009  reu8  3012  rmo3f  3013  sbc3an  3103  reu8nf  3123  rmo3  3134  ssalel  3225  ss2rab  3313  rabss  3314  ssrab  3315  dfdif3  3328  undi  3468  undif3ss  3481  difin2  3482  dfnul2  3509  disj  3556  disjsn  3750  snssb  3826  uni0c  3939  ssint  3964  iunss  4031  ssextss  4335  eqvinop  4358  opcom  4366  opeqsn  4368  opeqpr  4369  brabsb  4378  opelopabf  4392  opabm  4398  pofun  4432  sotritrieq  4445  uniuni  4571  ordsucim  4621  opeliunxp  4804  xpiundi  4807  brinxp2  4816  ssrel  4837  reliun  4872  cnvuni  4940  dmopab3  4968  opelres  5042  elres  5073  elsnres  5074  intirr  5148  ssrnres  5204  dminxp  5206  dfrel4v  5213  dmsnm  5227  rnco  5268  sb8iota  5319  dffun2  5361  dffun4f  5367  funco  5391  funcnveq  5418  fun11  5422  isarep1  5441  dff1o4  5621  dff1o6  5948  oprabid  6081  mpo2eqb  6162  ralrnmpo  6167  rexrnmpo  6168  opabex3d  6313  opabex3  6314  xporderlem  6426  f1od2  6430  tfr0dm  6552  tfrexlem  6564  frec0g  6627  nnaord  6741  ecid  6831  mptelixpg  6968  elixpsn  6969  mapsnen  7052  xpsnen  7071  xpcomco  7076  xpassen  7080  exmidontriimlem3  7529  nqnq0  7755  opelreal  8141  pitoregt0  8163  elnn0  9497  elxnn0  9564  elxr  10108  xrnepnf  10110  elfzuzb  10352  4fvwrd4  10473  elfzo2  10483  swrdnd  11347  resqrexlemsqa  11705  fisumcom2  12120  modfsummod  12140  fprodcom2fi  12308  nnwosdc  12731  isprm2  12810  isprm4  12812  pythagtriplem2  12960  4sqlem12  13096  isnsg2  13912  isnsg4  13921  dfrhm2  14291  cnfldui  14729  ntreq0  14989  txbas  15115  metrest  15363  2lgslem4  15968  umgr2edg1  16196  isclwwlk  16381  isclwwlknx  16403  clwwlkn1  16405  clwwlkn2  16408  clwwlknonel  16419  iseupthf1o  16435