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  5375  dfmpt3  5381  fnopabg  5382  fintm  5444  fin  5445  fores  5491  dff1o3  5511  fun11iun  5526  f11o  5538  f1ompt  5714  fsn  5735  imaiun  5808  isores2  5861  eqoprab2b  5981  opabex3d  6179  opabex3  6180  dfopab2  6248  dfoprab3s  6249  fmpox  6259  tpostpos  6323  dfsmo2  6346  qsid  6660  mapval2  6738  mapsncnv  6755  elixp2  6762  ixpin  6783  xpassen  6890  diffitest  6949  pw1dc0el  6973  supmoti  7060  eqinfti  7087  distrnqg  7456  ltbtwnnq  7485  distrnq0  7528  nqprrnd  7612  ltresr  7908  elznn0nn  9342  xrnemnf  9854  xrnepnf  9855  elioomnf  10045  elxrge0  10055  elfzuzb  10096  fzass4  10139  elfz2nn0  10189  elfzo2  10227  elfzo3  10241  lbfzo0  10259  fzind2  10317  infssuzex  10325  dfrp2  10355  rexfiuz  11156  fisumcom2  11605  prodmodc  11745  fprodcom2fi  11793  4sqlem12  12581  infpn2  12683  xpsfrnel  12997  xpscf  13000  islmod  13857  isbasis2g  14291  tgval2  14297  ntreq0  14378  txuni2  14502  isms2  14700  plyun0  14982  bdceq  15498