Theorem 3bitri 206

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitri.1	|- ( ph <-> ps )
3bitri.2	|- ( ps <-> ch )
3bitri.3	|- ( ch <-> th )

Assertion

Ref	Expression
3bitri	|- ( ph <-> th )

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 |- ( ph <-> ps )
2		3bitri.2	. . 3 |- ( ps <-> ch )
3		3bitri.3	. . 3 |- ( ch <-> th )
4	2, 3	bitri 184	. 2 |- ( ps <-> th )
5	1, 4	bitri 184	1 |- ( ph <-> th )

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  5916  oprabid  6049  mpo2eqb  6130  ralrnmpo  6135  rexrnmpo  6136  opabex3d  6282  opabex3  6283  xporderlem  6395  f1od2  6399  tfr0dm  6487  tfrexlem  6499  frec0g  6562  nnaord  6676  ecid  6766  mptelixpg  6902  elixpsn  6903  mapsnen  6985  xpsnen  7004  xpcomco  7009  xpassen  7013  exmidontriimlem3  7437  nqnq0  7660  opelreal  8046  pitoregt0  8068  elnn0  9403  elxnn0  9466  elxr  10010  xrnepnf  10012  elfzuzb  10253  4fvwrd4  10374  elfzo2  10384  swrdnd  11239  resqrexlemsqa  11584  fisumcom2  11998  modfsummod  12018  fprodcom2fi  12186  nnwosdc  12609  isprm2  12688  isprm4  12690  pythagtriplem2  12838  4sqlem12  12974  isnsg2  13789  isnsg4  13798  dfrhm2  14167  cnfldui  14602  ntreq0  14855  txbas  14981  metrest  15229  2lgslem4  15831  umgr2edg1  16059  isclwwlk  16244  isclwwlknx  16266  clwwlkn1  16268  clwwlkn2  16271  clwwlknonel  16282  iseupthf1o  16298