Theorem 3bitri 205

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 183	. 2 |- ( ps <-> th )
5	1, 4	bitri 183	1 |- ( ph <-> th )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1i  227  an32  551  orbi1i  752  orass  756  or32  759  dcan  918  dn1dc  944  an6  1299  excxor  1356  trubifal  1394  truxortru  1397  truxorfal  1398  falxortru  1399  falxorfal  1400  alrot4  1462  excom13  1667  sborv  1862  3exdistr  1887  4exdistr  1888  eeeanv  1905  ee4anv  1906  ee8anv  1907  sb3an  1931  elsb3  1951  elsb4  1952  sb9  1954  sbnf2  1956  sbco4  1982  2exsb  1984  sb8eu  2012  sb8euh  2022  sbmo  2058  2eu4  2092  2eu7  2093  r19.26-3  2562  rexcom13  2596  cbvreu  2652  ceqsex2  2726  ceqsex4v  2729  spc3gv  2778  ralrab2  2849  rexrab2  2851  reu2  2872  rmo4  2877  reu8  2880  rmo3f  2881  sbc3an  2970  rmo3  3000  dfss2  3086  ss2rab  3173  rabss  3174  ssrab  3175  dfdif3  3186  undi  3324  undif3ss  3337  difin2  3338  dfnul2  3365  disj  3411  disjsn  3585  uni0c  3762  ssint  3787  iunss  3854  ssextss  4142  eqvinop  4165  opcom  4172  opeqsn  4174  opeqpr  4175  brabsb  4183  opelopabf  4196  opabm  4202  pofun  4234  sotritrieq  4247  uniuni  4372  ordsucim  4416  opeliunxp  4594  xpiundi  4597  brinxp2  4606  ssrel  4627  reliun  4660  cnvuni  4725  dmopab3  4752  opelres  4824  elres  4855  elsnres  4856  intirr  4925  ssrnres  4981  dminxp  4983  dfrel4v  4990  dmsnm  5004  rnco  5045  sb8iota  5095  dffun2  5133  dffun4f  5139  funco  5163  funcnveq  5186  fun11  5190  isarep1  5209  dff1o4  5375  dff1o6  5677  oprabid  5803  mpo2eqb  5880  ralrnmpo  5885  rexrnmpo  5886  opabex3d  6019  opabex3  6020  xporderlem  6128  f1od2  6132  tfr0dm  6219  tfrexlem  6231  frec0g  6294  nnaord  6405  ecid  6492  mptelixpg  6628  elixpsn  6629  mapsnen  6705  xpsnen  6715  xpcomco  6720  xpassen  6724  nqnq0  7249  opelreal  7635  pitoregt0  7657  elnn0  8979  elxnn0  9042  elxr  9563  xrnepnf  9565  elfzuzb  9800  4fvwrd4  9917  elfzo2  9927  resqrexlemsqa  10796  fisumcom2  11207  modfsummod  11227  isprm2  11798  isprm4  11800  ntreq0  12301  txbas  12427  metrest  12675