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  768  orass  772  or32  775  dn1dc  966  an6  1355  excxor  1420  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  alrot4  1532  excom13  1735  sborv  1937  3exdistr  1962  4exdistr  1963  eeeanv  1984  ee4anv  1985  ee8anv  1986  sb3an  2009  sb9  2030  sbnf2  2032  sbco4  2058  2exsb  2060  sb8eu  2090  sb8euh  2100  sbmo  2137  2eu4  2171  2eu7  2172  elsb1  2207  elsb2  2208  r19.26-3  2661  rexcom13  2697  cbvreu  2763  ceqsex2  2842  ceqsex4v  2845  spc3gv  2897  ralrab2  2969  rexrab2  2971  reu2  2992  rmo4  2997  reu8  3000  rmo3f  3001  sbc3an  3091  reu8nf  3111  rmo3  3122  ssalel  3213  ss2rab  3301  rabss  3302  ssrab  3303  dfdif3  3315  undi  3453  undif3ss  3466  difin2  3467  dfnul2  3494  disj  3541  disjsn  3729  snssb  3804  uni0c  3917  ssint  3942  iunss  4009  ssextss  4310  eqvinop  4333  opcom  4341  opeqsn  4343  opeqpr  4344  brabsb  4353  opelopabf  4367  opabm  4373  pofun  4407  sotritrieq  4420  uniuni  4546  ordsucim  4596  opeliunxp  4779  xpiundi  4782  brinxp2  4791  ssrel  4812  reliun  4846  cnvuni  4914  dmopab3  4942  opelres  5016  elres  5047  elsnres  5048  intirr  5121  ssrnres  5177  dminxp  5179  dfrel4v  5186  dmsnm  5200  rnco  5241  sb8iota  5292  dffun2  5334  dffun4f  5340  funco  5364  funcnveq  5390  fun11  5394  isarep1  5413  dff1o4  5588  dff1o6  5912  oprabid  6045  mpo2eqb  6126  ralrnmpo  6131  rexrnmpo  6132  opabex3d  6278  opabex3  6279  xporderlem  6391  f1od2  6395  tfr0dm  6483  tfrexlem  6495  frec0g  6558  nnaord  6672  ecid  6762  mptelixpg  6898  elixpsn  6899  mapsnen  6981  xpsnen  7000  xpcomco  7005  xpassen  7009  exmidontriimlem3  7431  nqnq0  7654  opelreal  8040  pitoregt0  8062  elnn0  9397  elxnn0  9460  elxr  10004  xrnepnf  10006  elfzuzb  10247  4fvwrd4  10368  elfzo2  10378  swrdnd  11233  resqrexlemsqa  11578  fisumcom2  11992  modfsummod  12012  fprodcom2fi  12180  nnwosdc  12603  isprm2  12682  isprm4  12684  pythagtriplem2  12832  4sqlem12  12968  isnsg2  13783  isnsg4  13792  dfrhm2  14161  cnfldui  14596  ntreq0  14849  txbas  14975  metrest  15223  2lgslem4  15825  umgr2edg1  16053  isclwwlk  16203  isclwwlknx  16225  clwwlkn1  16227  clwwlkn2  16230  clwwlknonel  16241  iseupthf1o  16257