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  3466  eldifpr  3608  rexsns  3620  reusn  3652  prss  3734  tpss  3743  eluni2  3798  elunirab  3807  uniun  3813  uni0b  3819  unissb  3824  elintrab  3841  ssintrab  3852  intun  3860  intpr  3861  iuncom  3877  iuncom4  3878  iunab  3917  ssiinf  3920  iinab  3932  iunin2  3934  iunun  3949  iunxun  3950  iunxiun  3952  sspwuni  3955  iinpw  3961  cbvdisj  3974  brun  4038  brin  4039  brdif  4040  dftr2  4087  inuni  4139  repizf2lem  4145  unidif0  4151  ssext  4204  pweqb  4206  otth2  4224  opelopabsbALT  4242  eqopab2b  4262  pwin  4265  unisuc  4396  elpwpwel  4458  sucexb  4479  elomssom  4587  xpiundi  4667  xpiundir  4668  poinxp  4678  soinxp  4679  seinxp  4680  inopab  4741  difopab  4742  raliunxp  4750  rexiunxp  4751  iunxpf  4757  cnvco  4794  dmiun  4818  dmuni  4819  dm0rn0  4826  brres  4895  dmres  4910  cnvsym  4992  asymref  4994  codir  4997  qfto  4998  cnvopab  5010  cnvdif  5015  rniun  5019  dminss  5023  imainss  5024  cnvcnvsn  5085  resco  5113  imaco  5114  rnco  5115  coiun  5118  coass  5127  ressn  5149  cnviinm  5150  xpcom  5155  funcnv  5257  funcnv3  5258  fncnv  5262  fun11  5263  fnres  5312  dfmpt3  5318  fnopabg  5319  fintm  5381  fin  5382  fores  5427  dff1o3  5446  fun11iun  5461  f11o  5473  f1ompt  5644  fsn  5665  imaiun  5736  isores2  5789  eqoprab2b  5908  opabex3d  6097  opabex3  6098  dfopab2  6165  dfoprab3s  6166  fmpox  6176  tpostpos  6240  dfsmo2  6263  qsid  6574  mapval2  6652  mapsncnv  6669  elixp2  6676  ixpin  6697  xpassen  6804  diffitest  6861  pw1dc0el  6885  supmoti  6966  eqinfti  6993  distrnqg  7336  ltbtwnnq  7365  distrnq0  7408  nqprrnd  7492  ltresr  7788  elznn0nn  9213  xrnemnf  9721  xrnepnf  9722  elioomnf  9912  elxrge0  9922  elfzuzb  9962  fzass4  10005  elfz2nn0  10055  elfzo2  10093  elfzo3  10106  lbfzo0  10124  fzind2  10182  dfrp2  10207  rexfiuz  10940  fisumcom2  11388  prodmodc  11528  fprodcom2fi  11576  infssuzex  11891  infpn2  12398  isbasis2g  12758  tgval2  12766  ntreq0  12847  txuni2  12971  isms2  13169  bdceq  13799