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  770  orass  774  or32  777  dn1dc  968  an6  1357  excxor  1422  trubifal  1460  truxortru  1463  truxorfal  1464  falxortru  1465  falxorfal  1466  alrot4  1534  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  2663  rexcom13  2699  cbvreu  2765  ceqsex2  2844  ceqsex4v  2847  spc3gv  2899  ralrab2  2971  rexrab2  2973  reu2  2994  rmo4  2999  reu8  3002  rmo3f  3003  sbc3an  3093  reu8nf  3113  rmo3  3124  ssalel  3215  ss2rab  3303  rabss  3304  ssrab  3305  dfdif3  3317  undi  3455  undif3ss  3468  difin2  3469  dfnul2  3496  disj  3543  disjsn  3731  snssb  3806  uni0c  3919  ssint  3944  iunss  4011  ssextss  4312  eqvinop  4335  opcom  4343  opeqsn  4345  opeqpr  4346  brabsb  4355  opelopabf  4369  opabm  4375  pofun  4409  sotritrieq  4422  uniuni  4548  ordsucim  4598  opeliunxp  4781  xpiundi  4784  brinxp2  4793  ssrel  4814  reliun  4848  cnvuni  4916  dmopab3  4944  opelres  5018  elres  5049  elsnres  5050  intirr  5123  ssrnres  5179  dminxp  5181  dfrel4v  5188  dmsnm  5202  rnco  5243  sb8iota  5294  dffun2  5336  dffun4f  5342  funco  5366  funcnveq  5393  fun11  5397  isarep1  5416  dff1o4  5591  dff1o6  5917  oprabid  6050  mpo2eqb  6131  ralrnmpo  6136  rexrnmpo  6137  opabex3d  6283  opabex3  6284  xporderlem  6396  f1od2  6400  tfr0dm  6488  tfrexlem  6500  frec0g  6563  nnaord  6677  ecid  6767  mptelixpg  6903  elixpsn  6904  mapsnen  6986  xpsnen  7005  xpcomco  7010  xpassen  7014  exmidontriimlem3  7438  nqnq0  7661  opelreal  8047  pitoregt0  8069  elnn0  9404  elxnn0  9467  elxr  10011  xrnepnf  10013  elfzuzb  10254  4fvwrd4  10375  elfzo2  10385  swrdnd  11244  resqrexlemsqa  11589  fisumcom2  12004  modfsummod  12024  fprodcom2fi  12192  nnwosdc  12615  isprm2  12694  isprm4  12696  pythagtriplem2  12844  4sqlem12  12980  isnsg2  13795  isnsg4  13804  dfrhm2  14174  cnfldui  14609  ntreq0  14862  txbas  14988  metrest  15236  2lgslem4  15838  umgr2edg1  16066  isclwwlk  16251  isclwwlknx  16273  clwwlkn1  16275  clwwlkn2  16278  clwwlknonel  16289  iseupthf1o  16305