Theorem 3bitr4i 211

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3bitr4i.1	|- ( ph <-> ps )
3bitr4i.2	|- ( ch <-> ph )
3bitr4i.3	|- ( th <-> ps )

Assertion

Ref	Expression
3bitr4i	|- ( ch <-> th )

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 |- ( ch <-> ph )
2		3bitr4i.1	. . 3 |- ( ph <-> ps )
3		3bitr4i.3	. . 3 |- ( th <-> ps )
4	2, 3	bitr4i 186	. 2 |- ( ph <-> th )
5	1, 4	bitri 183	1 |- ( ch <-> 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:  bibi2d  231  pm4.71  387  pm5.32ri  452  mpan10  471  an31  559  an4  581  or4  766  ordir  812  andir  814  3anrot  978  3orrot  979  3ancoma  980  3orcomb  982  3ioran  988  3anbi123i  1183  3orbi123i  1184  3or6  1318  xorcom  1383  nfbii  1466  19.26-3an  1476  alnex  1492  19.42h  1680  19.42  1681  equsal  1720  equsalv  1786  sb6  1879  eeeanv  1926  sbbi  1952  sbco3xzyz  1966  sbcom2v  1978  sbel2x  1991  sb8eu  2032  sb8mo  2033  sb8euh  2042  eu1  2044  cbvmo  2059  mo3h  2072  sbmo  2078  eqcom  2172  abeq1  2280  cbvabw  2293  cbvab  2294  clelab  2296  nfceqi  2308  sbabel  2339  ralbii2  2480  rexbii2  2481  r2alf  2487  r2exf  2488  nfraldya  2505  nfrexdya  2506  r3al  2514  r19.41  2625  r19.42v  2627  ralcomf  2631  rexcomf  2632  reean  2638  3reeanv  2640  rabid2  2646  rabbi  2647  reubiia  2654  rmobiia  2659  reu5  2682  rmo5  2685  cbvralfw  2687  cbvrexfw  2688  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvrmo  2695  cbvralvw  2700  cbvrexvw  2701  vjust  2731  ceqsex3v  2772  ceqsex4v  2773  ceqsex8v  2775  eueq  2901  reu2  2918  reu6  2919  reu3  2920  rmo4  2923  rmo3f  2927  2rmorex  2936  cbvsbcw  2982  cbvsbc  2983  sbccomlem  3029  rmo3  3046  csbcow  3060  csbabg  3110  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  eqss  3162  uniiunlem  3236  ssequn1  3297  unss  3301  rexun  3307  ralunb  3308  elin3  3318  incom  3319  inass  3337  ssin  3349  ssddif  3361  unssdif  3362  difin  3364  invdif  3369  indif  3370  indi  3374  symdifxor  3393  disj3  3467  eldifpr  3610  rexsns  3622  reusn  3654  prss  3736  tpss  3745  eluni2  3800  elunirab  3809  uniun  3815  uni0b  3821  unissb  3826  elintrab  3843  ssintrab  3854  intun  3862  intpr  3863  iuncom  3879  iuncom4  3880  iunab  3919  ssiinf  3922  iinab  3934  iunin2  3936  iunun  3951  iunxun  3952  iunxiun  3954  sspwuni  3957  iinpw  3963  cbvdisj  3976  brun  4040  brin  4041  brdif  4042  dftr2  4089  inuni  4141  repizf2lem  4147  unidif0  4153  ssext  4206  pweqb  4208  otth2  4226  opelopabsbALT  4244  eqopab2b  4264  pwin  4267  unisuc  4398  elpwpwel  4460  sucexb  4481  elomssom  4589  xpiundi  4669  xpiundir  4670  poinxp  4680  soinxp  4681  seinxp  4682  inopab  4743  difopab  4744  raliunxp  4752  rexiunxp  4753  iunxpf  4759  cnvco  4796  dmiun  4820  dmuni  4821  dm0rn0  4828  brres  4897  dmres  4912  cnvsym  4994  asymref  4996  codir  4999  qfto  5000  cnvopab  5012  cnvdif  5017  rniun  5021  dminss  5025  imainss  5026  cnvcnvsn  5087  resco  5115  imaco  5116  rnco  5117  coiun  5120  coass  5129  ressn  5151  cnviinm  5152  xpcom  5157  funcnv  5259  funcnv3  5260  fncnv  5264  fun11  5265  fnres  5314  dfmpt3  5320  fnopabg  5321  fintm  5383  fin  5384  fores  5429  dff1o3  5448  fun11iun  5463  f11o  5475  f1ompt  5647  fsn  5668  imaiun  5739  isores2  5792  eqoprab2b  5911  opabex3d  6100  opabex3  6101  dfopab2  6168  dfoprab3s  6169  fmpox  6179  tpostpos  6243  dfsmo2  6266  qsid  6578  mapval2  6656  mapsncnv  6673  elixp2  6680  ixpin  6701  xpassen  6808  diffitest  6865  pw1dc0el  6889  supmoti  6970  eqinfti  6997  distrnqg  7349  ltbtwnnq  7378  distrnq0  7421  nqprrnd  7505  ltresr  7801  elznn0nn  9226  xrnemnf  9734  xrnepnf  9735  elioomnf  9925  elxrge0  9935  elfzuzb  9975  fzass4  10018  elfz2nn0  10068  elfzo2  10106  elfzo3  10119  lbfzo0  10137  fzind2  10195  dfrp2  10220  rexfiuz  10953  fisumcom2  11401  prodmodc  11541  fprodcom2fi  11589  infssuzex  11904  infpn2  12411  isbasis2g  12837  tgval2  12845  ntreq0  12926  txuni2  13050  isms2  13248  bdceq  13877