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  1510  excom13  1713  sborv  1915  3exdistr  1940  4exdistr  1941  eeeanv  1962  ee4anv  1963  ee8anv  1964  sb3an  1987  sb9  2008  sbnf2  2010  sbco4  2036  2exsb  2038  sb8eu  2068  sb8euh  2078  sbmo  2115  2eu4  2149  2eu7  2150  elsb1  2185  elsb2  2186  r19.26-3  2638  rexcom13  2674  cbvreu  2740  ceqsex2  2818  ceqsex4v  2821  spc3gv  2873  ralrab2  2945  rexrab2  2947  reu2  2968  rmo4  2973  reu8  2976  rmo3f  2977  sbc3an  3067  reu8nf  3087  rmo3  3098  ssalel  3189  ss2rab  3277  rabss  3278  ssrab  3279  dfdif3  3291  undi  3429  undif3ss  3442  difin2  3443  dfnul2  3470  disj  3517  disjsn  3705  snssb  3777  uni0c  3890  ssint  3915  iunss  3982  ssextss  4282  eqvinop  4305  opcom  4313  opeqsn  4315  opeqpr  4316  brabsb  4325  opelopabf  4339  opabm  4345  pofun  4377  sotritrieq  4390  uniuni  4516  ordsucim  4566  opeliunxp  4748  xpiundi  4751  brinxp2  4760  ssrel  4781  reliun  4814  cnvuni  4882  dmopab3  4910  opelres  4983  elres  5014  elsnres  5015  intirr  5088  ssrnres  5144  dminxp  5146  dfrel4v  5153  dmsnm  5167  rnco  5208  sb8iota  5258  dffun2  5300  dffun4f  5306  funco  5330  funcnveq  5356  fun11  5360  isarep1  5379  dff1o4  5552  dff1o6  5868  oprabid  5999  mpo2eqb  6078  ralrnmpo  6083  rexrnmpo  6084  opabex3d  6229  opabex3  6230  xporderlem  6340  f1od2  6344  tfr0dm  6431  tfrexlem  6443  frec0g  6506  nnaord  6618  ecid  6708  mptelixpg  6844  elixpsn  6845  mapsnen  6927  xpsnen  6941  xpcomco  6946  xpassen  6950  exmidontriimlem3  7366  nqnq0  7589  opelreal  7975  pitoregt0  7997  elnn0  9332  elxnn0  9395  elxr  9933  xrnepnf  9935  elfzuzb  10176  4fvwrd4  10297  elfzo2  10307  swrdnd  11150  resqrexlemsqa  11450  fisumcom2  11864  modfsummod  11884  fprodcom2fi  12052  nnwosdc  12475  isprm2  12554  isprm4  12556  pythagtriplem2  12704  4sqlem12  12840  isnsg2  13654  isnsg4  13663  dfrhm2  14031  cnfldui  14466  ntreq0  14719  txbas  14845  metrest  15093  2lgslem4  15695