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  4264  eqvinop  4287  opcom  4295  opeqsn  4297  opeqpr  4298  brabsb  4307  opelopabf  4321  opabm  4327  pofun  4359  sotritrieq  4372  uniuni  4498  ordsucim  4548  opeliunxp  4730  xpiundi  4733  brinxp2  4742  ssrel  4763  reliun  4796  cnvuni  4864  dmopab3  4891  opelres  4964  elres  4995  elsnres  4996  intirr  5069  ssrnres  5125  dminxp  5127  dfrel4v  5134  dmsnm  5148  rnco  5189  sb8iota  5239  dffun2  5281  dffun4f  5287  funco  5311  funcnveq  5337  fun11  5341  isarep1  5360  dff1o4  5530  dff1o6  5845  oprabid  5976  mpo2eqb  6055  ralrnmpo  6060  rexrnmpo  6061  opabex3d  6206  opabex3  6207  xporderlem  6317  f1od2  6321  tfr0dm  6408  tfrexlem  6420  frec0g  6483  nnaord  6595  ecid  6685  mptelixpg  6821  elixpsn  6822  mapsnen  6903  xpsnen  6916  xpcomco  6921  xpassen  6925  exmidontriimlem3  7335  nqnq0  7554  opelreal  7940  pitoregt0  7962  elnn0  9297  elxnn0  9360  elxr  9898  xrnepnf  9900  elfzuzb  10141  4fvwrd4  10262  elfzo2  10272  swrdnd  11112  resqrexlemsqa  11335  fisumcom2  11749  modfsummod  11769  fprodcom2fi  11937  nnwosdc  12360  isprm2  12439  isprm4  12441  pythagtriplem2  12589  4sqlem12  12725  isnsg2  13539  isnsg4  13548  dfrhm2  13916  cnfldui  14351  ntreq0  14604  txbas  14730  metrest  14978  2lgslem4  15580