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  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  7498  nqnq0  7721  opelreal  8107  pitoregt0  8129  elnn0  9463  elxnn0  9528  elxr  10072  xrnepnf  10074  elfzuzb  10316  4fvwrd4  10437  elfzo2  10447  swrdnd  11306  resqrexlemsqa  11664  fisumcom2  12079  modfsummod  12099  fprodcom2fi  12267  nnwosdc  12690  isprm2  12769  isprm4  12771  pythagtriplem2  12919  4sqlem12  13055  isnsg2  13870  isnsg4  13879  dfrhm2  14249  cnfldui  14685  ntreq0  14943  txbas  15069  metrest  15317  2lgslem4  15922  umgr2edg1  16150  isclwwlk  16335  isclwwlknx  16357  clwwlkn1  16359  clwwlkn2  16362  clwwlknonel  16373  iseupthf1o  16389