Theorem 3bitr4i 212

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 187	. 2 |- ( ph <-> th )
5	1, 4	bitri 184	1 |- ( ch <-> 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:  bibi2d  232  pm4.71  389  pm5.32ri  455  mpan10  474  an31  564  an4  586  or4  772  ordir  818  andir  820  3anrot  985  3orrot  986  3ancoma  987  3orcomb  989  3ioran  995  3anbi123i  1190  3orbi123i  1191  3or6  1334  xorcom  1399  nfbii  1487  19.26-3an  1497  alnex  1513  19.42h  1701  19.42  1702  equsal  1741  equsalv  1807  sb6  1901  eeeanv  1952  sbbi  1978  sbco3xzyz  1992  sbcom2v  2004  sbel2x  2017  sb8eu  2058  sb8mo  2059  sb8euh  2068  eu1  2070  cbvmo  2085  mo3h  2098  sbmo  2104  eqcom  2198  abeq1  2306  cbvabw  2319  cbvab  2320  clelab  2322  nfceqi  2335  sbabel  2366  ralbii2  2507  rexbii2  2508  r2alf  2514  r2exf  2515  nfraldya  2532  nfrexdya  2533  r3al  2541  r19.41  2652  r19.42v  2654  ralcomf  2658  rexcomf  2659  reean  2666  3reeanv  2668  rabid2  2674  rabbi  2675  reubiia  2682  rmobiia  2687  reu5  2714  rmo5  2717  cbvralfw  2719  cbvrexfw  2720  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrmo  2728  cbvralvw  2733  cbvrexvw  2734  vjust  2764  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  eueq  2935  reu2  2952  reu6  2953  reu3  2954  rmo4  2957  rmo3f  2961  2rmorex  2970  cbvsbcw  3017  cbvsbc  3018  sbccomlem  3064  rmo3  3081  csbcow  3095  csbabg  3146  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  eqss  3199  uniiunlem  3273  ssequn1  3334  unss  3338  rexun  3344  ralunb  3345  elin3  3355  incom  3356  inass  3374  ssin  3386  ssddif  3398  unssdif  3399  difin  3401  invdif  3406  indif  3407  indi  3411  symdifxor  3430  disj3  3504  eldifpr  3650  rexsns  3662  reusn  3694  prss  3779  tpss  3789  eluni2  3844  elunirab  3853  uniun  3859  uni0b  3865  unissb  3870  elintrab  3887  ssintrab  3898  intun  3906  intpr  3907  iuncom  3923  iuncom4  3924  iunab  3964  ssiinf  3967  iinab  3979  iunin2  3981  iunun  3996  iunxun  3997  iunxiun  3999  sspwuni  4002  iinpw  4008  cbvdisj  4021  brun  4085  brin  4086  brdif  4087  dftr2  4134  inuni  4189  repizf2lem  4195  unidif0  4201  ssext  4255  pweqb  4257  otth2  4275  opelopabsbALT  4294  eqopab2b  4315  pwin  4318  unisuc  4449  elpwpwel  4511  sucexb  4534  elomssom  4642  xpiundi  4722  xpiundir  4723  poinxp  4733  soinxp  4734  seinxp  4735  inopab  4799  difopab  4800  raliunxp  4808  rexiunxp  4809  iunxpf  4815  cnvco  4852  dmiun  4876  dmuni  4877  dm0rn0  4884  brres  4953  dmres  4968  restidsing  5003  cnvsym  5054  asymref  5056  codir  5059  qfto  5060  cnvopab  5072  cnvdif  5077  rniun  5081  dminss  5085  imainss  5086  cnvcnvsn  5147  resco  5175  imaco  5176  rnco  5177  coiun  5180  coass  5189  ressn  5211  cnviinm  5212  xpcom  5217  funcnv  5320  funcnv3  5321  fncnv  5325  fun11  5326  fnres  5377  dfmpt3  5383  fnopabg  5384  fintm  5446  fin  5447  fores  5493  dff1o3  5513  fun11iun  5528  f11o  5540  f1ompt  5716  fsn  5737  imaiun  5810  isores2  5863  eqoprab2b  5984  opabex3d  6187  opabex3  6188  dfopab2  6256  dfoprab3s  6257  fmpox  6267  tpostpos  6331  dfsmo2  6354  qsid  6668  mapval2  6746  mapsncnv  6763  elixp2  6770  ixpin  6791  xpassen  6898  diffitest  6957  pw1dc0el  6981  supmoti  7068  eqinfti  7095  distrnqg  7471  ltbtwnnq  7500  distrnq0  7543  nqprrnd  7627  ltresr  7923  elznn0nn  9357  xrnemnf  9869  xrnepnf  9870  elioomnf  10060  elxrge0  10070  elfzuzb  10111  fzass4  10154  elfz2nn0  10204  elfzo2  10242  elfzo3  10256  lbfzo0  10274  fzind2  10332  infssuzex  10340  dfrp2  10370  rexfiuz  11171  fisumcom2  11620  prodmodc  11760  fprodcom2fi  11808  4sqlem12  12596  infpn2  12698  xpsfrnel  13046  xpscf  13049  islmod  13923  isbasis2g  14365  tgval2  14371  ntreq0  14452  txuni2  14576  isms2  14774  plyun0  15056  bdceq  15572