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  771  ordir  817  andir  819  3anrot  983  3orrot  984  3ancoma  985  3orcomb  987  3ioran  993  3anbi123i  1188  3orbi123i  1189  3or6  1323  xorcom  1388  nfbii  1473  19.26-3an  1483  alnex  1499  19.42h  1687  19.42  1688  equsal  1727  equsalv  1793  sb6  1886  eeeanv  1933  sbbi  1959  sbco3xzyz  1973  sbcom2v  1985  sbel2x  1998  sb8eu  2039  sb8mo  2040  sb8euh  2049  eu1  2051  cbvmo  2066  mo3h  2079  sbmo  2085  eqcom  2179  abeq1  2287  cbvabw  2300  cbvab  2301  clelab  2303  nfceqi  2315  sbabel  2346  ralbii2  2487  rexbii2  2488  r2alf  2494  r2exf  2495  nfraldya  2512  nfrexdya  2513  r3al  2521  r19.41  2632  r19.42v  2634  ralcomf  2638  rexcomf  2639  reean  2646  3reeanv  2648  rabid2  2654  rabbi  2655  reubiia  2662  rmobiia  2667  reu5  2690  rmo5  2693  cbvralfw  2695  cbvrexfw  2696  cbvralf  2697  cbvrexf  2698  cbvreu  2703  cbvrmo  2704  cbvralvw  2709  cbvrexvw  2710  vjust  2740  ceqsex3v  2781  ceqsex4v  2782  ceqsex8v  2784  eueq  2910  reu2  2927  reu6  2928  reu3  2929  rmo4  2932  rmo3f  2936  2rmorex  2945  cbvsbcw  2992  cbvsbc  2993  sbccomlem  3039  rmo3  3056  csbcow  3070  csbabg  3120  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  eqss  3172  uniiunlem  3246  ssequn1  3307  unss  3311  rexun  3317  ralunb  3318  elin3  3328  incom  3329  inass  3347  ssin  3359  ssddif  3371  unssdif  3372  difin  3374  invdif  3379  indif  3380  indi  3384  symdifxor  3403  disj3  3477  eldifpr  3621  rexsns  3633  reusn  3665  prss  3750  tpss  3760  eluni2  3815  elunirab  3824  uniun  3830  uni0b  3836  unissb  3841  elintrab  3858  ssintrab  3869  intun  3877  intpr  3878  iuncom  3894  iuncom4  3895  iunab  3935  ssiinf  3938  iinab  3950  iunin2  3952  iunun  3967  iunxun  3968  iunxiun  3970  sspwuni  3973  iinpw  3979  cbvdisj  3992  brun  4056  brin  4057  brdif  4058  dftr2  4105  inuni  4157  repizf2lem  4163  unidif0  4169  ssext  4223  pweqb  4225  otth2  4243  opelopabsbALT  4261  eqopab2b  4281  pwin  4284  unisuc  4415  elpwpwel  4477  sucexb  4498  elomssom  4606  xpiundi  4686  xpiundir  4687  poinxp  4697  soinxp  4698  seinxp  4699  inopab  4761  difopab  4762  raliunxp  4770  rexiunxp  4771  iunxpf  4777  cnvco  4814  dmiun  4838  dmuni  4839  dm0rn0  4846  brres  4915  dmres  4930  restidsing  4965  cnvsym  5014  asymref  5016  codir  5019  qfto  5020  cnvopab  5032  cnvdif  5037  rniun  5041  dminss  5045  imainss  5046  cnvcnvsn  5107  resco  5135  imaco  5136  rnco  5137  coiun  5140  coass  5149  ressn  5171  cnviinm  5172  xpcom  5177  funcnv  5279  funcnv3  5280  fncnv  5284  fun11  5285  fnres  5334  dfmpt3  5340  fnopabg  5341  fintm  5403  fin  5404  fores  5449  dff1o3  5469  fun11iun  5484  f11o  5496  f1ompt  5669  fsn  5690  imaiun  5763  isores2  5816  eqoprab2b  5935  opabex3d  6124  opabex3  6125  dfopab2  6192  dfoprab3s  6193  fmpox  6203  tpostpos  6267  dfsmo2  6290  qsid  6602  mapval2  6680  mapsncnv  6697  elixp2  6704  ixpin  6725  xpassen  6832  diffitest  6889  pw1dc0el  6913  supmoti  6994  eqinfti  7021  distrnqg  7388  ltbtwnnq  7417  distrnq0  7460  nqprrnd  7544  ltresr  7840  elznn0nn  9269  xrnemnf  9779  xrnepnf  9780  elioomnf  9970  elxrge0  9980  elfzuzb  10021  fzass4  10064  elfz2nn0  10114  elfzo2  10152  elfzo3  10165  lbfzo0  10183  fzind2  10241  dfrp2  10266  rexfiuz  11000  fisumcom2  11448  prodmodc  11588  fprodcom2fi  11636  infssuzex  11952  infpn2  12459  xpsfrnel  12768  xpscf  12771  islmod  13386  isbasis2g  13584  tgval2  13590  ntreq0  13671  txuni2  13795  isms2  13993  bdceq  14633