Theorem 3bitr4g 221

Description: More general version of 3bitr4i 210. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
3bitr4g	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.2	. . 3 |- ( th <-> ps )
2		3bitr4g.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5bb 190	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 196	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi1d  231  pm5.32rd  438  orbi1d  737  dcbid  781  pm4.14dc  820  orbididc  894  3orbi123d  1242  3anbi123d  1243  xorbi2d  1311  xorbi1d  1312  nfbidf  1472  drnf1  1661  drnf2  1662  drsb1  1720  sbal2  1939  eubidh  1947  eubid  1948  mobidh  1975  mobid  1976  eqeq1  2087  eqeq2  2090  eleq1  2141  eleq2  2142  nfceqdf  2218  drnfc1  2235  drnfc2  2236  neeq1  2258  neeq2  2259  neleq1  2343  neleq2  2344  ralbida  2362  rexbida  2363  ralbidv2  2370  rexbidv2  2371  r19.21t  2436  r19.23t  2467  reubida  2535  rmobida  2540  raleqf  2545  rexeqf  2546  reueq1f  2547  rmoeq1f  2548  cbvraldva2  2581  cbvrexdva2  2582  dfsbcq  2817  sbcbi2  2864  sbcbid  2871  eqsbc3r  2874  sbcabel  2895  sbnfc2  2962  ssconb  3105  uneq1  3119  ineq1  3160  difin2  3226  reuun2  3247  reldisj  3295  undif4  3306  disjssun  3307  sbcssg  3350  eltpg  3438  raltpg  3445  rextpg  3446  r19.12sn  3458  opeq1  3570  opeq2  3571  intmin4  3664  dfiun2g  3710  iindif2m  3745  iinin2m  3746  breq  3787  breq1  3788  breq2  3789  treq  3881  opthg2  3994  poeq1  4054  soeq1  4070  frforeq1  4098  freq1  4099  frforeq2  4100  freq2  4101  frforeq3  4102  weeq1  4111  weeq2  4112  ordeq  4127  limeq  4132  rabxfrd  4219  iunpw  4229  opthprc  4409  releq  4440  sbcrel  4444  eqrel  4447  eqrelrel  4459  xpiindim  4491  brcnvg  4534  brresg  4638  resieq  4640  xpcanm  4780  xpcan2m  4781  dmsnopg  4812  dfco2a  4841  cnvpom  4880  cnvsom  4881  iotaeq  4895  sniota  4914  sbcfung  4945  fneq1  5007  fneq2  5008  feq1  5050  feq2  5051  feq3  5052  sbcfng  5064  sbcfg  5065  f1eq1  5107  f1eq2  5108  f1eq3  5109  foeq1  5122  foeq2  5123  foeq3  5124  f1oeq1  5137  f1oeq2  5138  f1oeq3  5139  fun11iun  5167  mpteqb  5282  dffo3  5335  fmptco  5351  dff13  5428  f1imaeq  5435  f1eqcocnv  5451  fliftcnv  5455  isoeq1  5461  isoeq2  5462  isoeq3  5463  isoeq4  5464  isoeq5  5465  isocnv2  5472  acexmid  5531  fnotovb  5568  mpt2eq123  5584  ottposg  5893  dmtpos  5894  smoeq  5928  nnacan  6108  nnmcan  6115  ereq1  6136  ereq2  6137  elecg  6167  ereldm  6172  enfi  6358  creur  8036  eqreznegel  8699  ltxr  8849  icoshftf1o  9013  elfzm11  9108  elfzomelpfzo  9240  nn0ennn  9425  nnesq  9592  rexfiuz  9875  cau4  10002  dvdsflip  10251  divgcdcoprm0  10483  cbvrald  10598  bj-dcbi  10719