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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1i  228  an32  568  orbi1i  775  orass  779  or32  782  dn1dc  973  an6  1362  excxor  1427  trubifal  1465  truxortru  1468  truxorfal  1469  falxortru  1470  falxorfal  1471  alrot4  1539  excom13  1741  sborv  1945  3exdistr  1971  4exdistr  1972  eeeanv  1993  ee4anv  1994  ee8anv  1995  sb3an  2018  sb9  2039  sbnf2  2041  sbco4  2067  2exsb  2069  sb8eu  2099  sb8euh  2109  sbmo  2146  2eu4  2180  2eu7  2181  elsb1  2216  elsb2  2217  r19.26-3  2681  rexcom13  2717  cbvreu  2784  ceqsex2  2863  ceqsex4v  2866  spc3gv  2918  ralrab2  2991  rexrab2  2993  reu2  3014  rmo4  3019  reu8  3022  rmo3f  3023  sbc3an  3113  reu8nf  3133  rmo3  3144  ssalel  3235  ss2rab  3324  rabss  3325  ssrab  3326  dfdif3  3339  undi  3479  undif3ss  3492  difin2  3493  disj  3573  disjsn  3771  snssb  3848  uni0c  3961  ssint  3986  iunss  4053  ssextss  4360  eqvinop  4383  opcom  4391  opeqsn  4393  opeqpr  4394  brabsb  4403  opelopabf  4417  opabm  4423  pofun  4457  sotritrieq  4470  uniuni  4597  ordsucim  4647  opeliunxp  4830  xpiundi  4833  brinxp2  4842  ssrel  4863  reliun  4898  cnvuni  4966  dmopab3  4994  opelres  5068  elres  5099  elsnres  5100  intirr  5174  ssrnres  5230  dminxp  5232  dfrel4v  5239  dmsnm  5253  rnco  5294  sb8iota  5345  dffun2  5387  dffun4f  5393  funco  5417  funcnveq  5444  fun11  5448  isarep1  5467  dff1o4  5647  dff1o6  5982  oprabid  6117  mpo2eqb  6198  ralrnmpo  6203  rexrnmpo  6204  opabex3d  6350  opabex3  6351  xporderlem  6467  f1od2  6471  tfr0dm  6593  tfrexlem  6605  frec0g  6668  nnaord  6782  ecid  6872  mptelixpg  7016  elixpsn  7017  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  exmidontriimlem3  7579  nqnq0  7808  opelreal  8194  pitoregt0  8216  elnn0  9565  elxnn0  9632  elxr  10178  xrnepnf  10180  elfzuzb  10422  4fvwrd4  10547  elfzo2  10557  swrdnd  11431  resqrexlemsqa  11790  fisumcom2  12205  modfsummod  12225  fprodcom2fi  12393  nnwosdc  12816  isprm2  12895  isprm4  12897  pythagtriplem2  13045  4sqlem12  13181  isnsg2  14006  isnsg4  14015  dfrhm2  14461  cnfldui  14924  isassa  15002  ntreq0  15233  txbas  15359  metrest  15607  2lgslem4  16222  umgr2edg1  16450  isclwwlk  16635  isclwwlknx  16657  clwwlkn1  16659  clwwlkn2  16662  clwwlknonel  16673  iseupthf1o  16689  alsanmo  17151  ralsanmo  17152