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  4362  eqvinop  4385  opcom  4393  opeqsn  4395  opeqpr  4396  brabsb  4405  opelopabf  4419  opabm  4425  pofun  4459  sotritrieq  4472  uniuni  4599  ordsucim  4649  opeliunxp  4832  xpiundi  4835  brinxp2  4844  ssrel  4865  reliun  4900  cnvuni  4968  dmopab3  4996  opelres  5070  elres  5101  elsnres  5102  intirr  5177  ssrnres  5233  dminxp  5235  dfrel4v  5242  dmsnm  5256  rnco  5297  sb8iota  5348  dffun2  5390  dffun4f  5396  funco  5420  funcnveq  5447  fun11  5451  isarep1  5470  dff1o4  5650  dff1o6  5985  oprabid  6120  mpo2eqb  6201  ralrnmpo  6206  rexrnmpo  6207  opabex3d  6354  opabex3  6355  xporderlem  6471  f1od2  6475  tfr0dm  6597  tfrexlem  6609  frec0g  6672  nnaord  6786  ecid  6876  mptelixpg  7020  elixpsn  7021  mapsnen  7104  xpsnen  7123  xpcomco  7128  xpassen  7132  exmidontriimlem3  7585  nqnq0  7814  opelreal  8200  pitoregt0  8222  elnn0  9576  elxnn0  9643  elxr  10195  xrnepnf  10197  elfzuzb  10439  4fvwrd4  10564  elfzo2  10574  swrdnd  11453  resqrexlemsqa  11812  fisumcom2  12230  modfsummod  12250  fprodcom2fi  12418  nnwosdc  12841  isprm2  12920  isprm4  12922  pythagtriplem2  13074  4sqlem12  13210  isnsg2  14065  isnsg4  14074  dfrhm2  14570  cnfldui  15033  isassa  15111  ntreq0  15358  txbas  15484  metrest  15732  2lgslem4  16427  umgr2edg1  16655  isclwwlk  16840  isclwwlknx  16862  clwwlkn1  16864  clwwlkn2  16867  clwwlknonel  16878  iseupthf1o  16894  alsanmo  17358  ralsanmo  17359