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  765  orass  769  or32  772  dn1dc  963  an6  1334  excxor  1398  trubifal  1436  truxortru  1439  truxorfal  1440  falxortru  1441  falxorfal  1442  alrot4  1509  excom13  1712  sborv  1914  3exdistr  1939  4exdistr  1940  eeeanv  1961  ee4anv  1962  ee8anv  1963  sb3an  1986  sb9  2007  sbnf2  2009  sbco4  2035  2exsb  2037  sb8eu  2067  sb8euh  2077  sbmo  2113  2eu4  2147  2eu7  2148  elsb1  2183  elsb2  2184  r19.26-3  2636  rexcom13  2672  cbvreu  2736  ceqsex2  2813  ceqsex4v  2816  spc3gv  2866  ralrab2  2938  rexrab2  2940  reu2  2961  rmo4  2966  reu8  2969  rmo3f  2970  sbc3an  3060  rmo3  3090  ssalel  3181  ss2rab  3269  rabss  3270  ssrab  3271  dfdif3  3283  undi  3421  undif3ss  3434  difin2  3435  dfnul2  3462  disj  3509  disjsn  3695  snssb  3766  uni0c  3876  ssint  3901  iunss  3968  ssextss  4265  eqvinop  4288  opcom  4296  opeqsn  4298  opeqpr  4299  brabsb  4308  opelopabf  4322  opabm  4328  pofun  4360  sotritrieq  4373  uniuni  4499  ordsucim  4549  opeliunxp  4731  xpiundi  4734  brinxp2  4743  ssrel  4764  reliun  4797  cnvuni  4865  dmopab3  4892  opelres  4965  elres  4996  elsnres  4997  intirr  5070  ssrnres  5126  dminxp  5128  dfrel4v  5135  dmsnm  5149  rnco  5190  sb8iota  5240  dffun2  5282  dffun4f  5288  funco  5312  funcnveq  5338  fun11  5342  isarep1  5361  dff1o4  5532  dff1o6  5847  oprabid  5978  mpo2eqb  6057  ralrnmpo  6062  rexrnmpo  6063  opabex3d  6208  opabex3  6209  xporderlem  6319  f1od2  6323  tfr0dm  6410  tfrexlem  6422  frec0g  6485  nnaord  6597  ecid  6687  mptelixpg  6823  elixpsn  6824  mapsnen  6905  xpsnen  6918  xpcomco  6923  xpassen  6927  exmidontriimlem3  7337  nqnq0  7556  opelreal  7942  pitoregt0  7964  elnn0  9299  elxnn0  9362  elxr  9900  xrnepnf  9902  elfzuzb  10143  4fvwrd4  10264  elfzo2  10274  swrdnd  11115  resqrexlemsqa  11368  fisumcom2  11782  modfsummod  11802  fprodcom2fi  11970  nnwosdc  12393  isprm2  12472  isprm4  12474  pythagtriplem2  12622  4sqlem12  12758  isnsg2  13572  isnsg4  13581  dfrhm2  13949  cnfldui  14384  ntreq0  14637  txbas  14763  metrest  15011  2lgslem4  15613