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  768  orass  772  or32  775  dn1dc  966  an6  1355  excxor  1420  trubifal  1458  truxortru  1461  truxorfal  1462  falxortru  1463  falxorfal  1464  alrot4  1532  excom13  1735  sborv  1937  3exdistr  1962  4exdistr  1963  eeeanv  1984  ee4anv  1985  ee8anv  1986  sb3an  2009  sb9  2030  sbnf2  2032  sbco4  2058  2exsb  2060  sb8eu  2090  sb8euh  2100  sbmo  2137  2eu4  2171  2eu7  2172  elsb1  2207  elsb2  2208  r19.26-3  2661  rexcom13  2697  cbvreu  2763  ceqsex2  2841  ceqsex4v  2844  spc3gv  2896  ralrab2  2968  rexrab2  2970  reu2  2991  rmo4  2996  reu8  2999  rmo3f  3000  sbc3an  3090  reu8nf  3110  rmo3  3121  ssalel  3212  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  undi  3452  undif3ss  3465  difin2  3466  dfnul2  3493  disj  3540  disjsn  3728  snssb  3801  uni0c  3914  ssint  3939  iunss  4006  ssextss  4306  eqvinop  4329  opcom  4337  opeqsn  4339  opeqpr  4340  brabsb  4349  opelopabf  4363  opabm  4369  pofun  4403  sotritrieq  4416  uniuni  4542  ordsucim  4592  opeliunxp  4774  xpiundi  4777  brinxp2  4786  ssrel  4807  reliun  4840  cnvuni  4908  dmopab3  4936  opelres  5010  elres  5041  elsnres  5042  intirr  5115  ssrnres  5171  dminxp  5173  dfrel4v  5180  dmsnm  5194  rnco  5235  sb8iota  5286  dffun2  5328  dffun4f  5334  funco  5358  funcnveq  5384  fun11  5388  isarep1  5407  dff1o4  5580  dff1o6  5900  oprabid  6033  mpo2eqb  6114  ralrnmpo  6119  rexrnmpo  6120  opabex3d  6266  opabex3  6267  xporderlem  6377  f1od2  6381  tfr0dm  6468  tfrexlem  6480  frec0g  6543  nnaord  6655  ecid  6745  mptelixpg  6881  elixpsn  6882  mapsnen  6964  xpsnen  6980  xpcomco  6985  xpassen  6989  exmidontriimlem3  7405  nqnq0  7628  opelreal  8014  pitoregt0  8036  elnn0  9371  elxnn0  9434  elxr  9972  xrnepnf  9974  elfzuzb  10215  4fvwrd4  10336  elfzo2  10346  swrdnd  11191  resqrexlemsqa  11535  fisumcom2  11949  modfsummod  11969  fprodcom2fi  12137  nnwosdc  12560  isprm2  12639  isprm4  12641  pythagtriplem2  12789  4sqlem12  12925  isnsg2  13740  isnsg4  13749  dfrhm2  14118  cnfldui  14553  ntreq0  14806  txbas  14932  metrest  15180  2lgslem4  15782  umgr2edg1  16007