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  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  7428  nqnq0  7651  opelreal  8037  pitoregt0  8059  elnn0  9394  elxnn0  9457  elxr  10001  xrnepnf  10003  elfzuzb  10244  4fvwrd4  10365  elfzo2  10375  swrdnd  11230  resqrexlemsqa  11575  fisumcom2  11989  modfsummod  12009  fprodcom2fi  12177  nnwosdc  12600  isprm2  12679  isprm4  12681  pythagtriplem2  12829  4sqlem12  12965  isnsg2  13780  isnsg4  13789  dfrhm2  14158  cnfldui  14593  ntreq0  14846  txbas  14972  metrest  15220  2lgslem4  15822  umgr2edg1  16048  isclwwlk  16189  isclwwlknx  16211  clwwlkn1  16213  clwwlkn2  16216  clwwlknonel  16227  iseupthf1o  16243