Theorem 3bitr4g 222

Description: More general version of 3bitr4i 211. 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 191	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 197	1 |- ( ph -> ( th <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1d  232  pm5.32rd  442  orbi1d  746  stbid  783  dcbid  792  pm4.14dc  831  orbididc  905  3orbi123d  1257  3anbi123d  1258  xorbi2d  1326  xorbi1d  1327  nfbidf  1487  drnf1  1679  drnf2  1680  drsb1  1738  sbal2  1958  eubidh  1966  eubid  1967  mobidh  1994  mobid  1995  eqeq1  2106  eqeq2  2109  eleq1w  2160  eleq2w  2161  eleq1  2162  eleq2  2163  nfceqdf  2239  drnfc1  2257  drnfc2  2258  neeq1  2280  neeq2  2281  neleq1  2366  neleq2  2367  dfrex2dc  2387  ralbida  2390  rexbida  2391  ralbidv2  2398  rexbidv2  2399  r19.21t  2466  r19.23t  2498  reubida  2570  rmobida  2575  raleqf  2580  rexeqf  2581  reueq1f  2582  rmoeq1f  2583  cbvraldva2  2616  cbvrexdva2  2617  dfsbcq  2864  sbcbi2  2911  sbcbid  2918  eqsbc3r  2921  sbcabel  2942  sbnfc2  3010  ssconb  3156  uneq1  3170  ineq1  3217  difin2  3285  reuun2  3306  reldisj  3361  undif4  3372  disjssun  3373  sbcssg  3419  eltpg  3516  raltpg  3523  rextpg  3524  r19.12sn  3536  opeq1  3652  opeq2  3653  intmin4  3746  dfiun2g  3792  iindif2m  3827  iinin2m  3828  breq  3877  breq1  3878  breq2  3879  treq  3972  opthg2  4099  poeq1  4159  soeq1  4175  frforeq1  4203  freq1  4204  frforeq2  4205  freq2  4206  frforeq3  4207  weeq1  4216  weeq2  4217  ordeq  4232  limeq  4237  rabxfrd  4328  iunpw  4339  opthprc  4528  releq  4559  sbcrel  4563  eqrel  4566  eqrelrel  4578  xpiindim  4614  brcnvg  4658  brresg  4763  resieq  4765  xpcanm  4914  xpcan2m  4915  dmsnopg  4946  dfco2a  4975  cnvpom  5017  cnvsom  5018  iotaeq  5032  sniota  5051  sbcfung  5083  fneq1  5147  fneq2  5148  feq1  5191  feq2  5192  feq3  5193  sbcfng  5206  sbcfg  5207  f1eq1  5259  f1eq2  5260  f1eq3  5261  foeq1  5277  foeq2  5278  foeq3  5279  f1oeq1  5292  f1oeq2  5293  f1oeq3  5294  fun11iun  5322  mpteqb  5443  dffo3  5499  fmptco  5518  dff13  5601  f1imaeq  5608  f1eqcocnv  5624  fliftcnv  5628  isoeq1  5634  isoeq2  5635  isoeq3  5636  isoeq4  5637  isoeq5  5638  isocnv2  5645  acexmid  5705  fnotovb  5746  mpoeq123  5762  ottposg  6082  dmtpos  6083  smoeq  6117  nnacan  6338  nnmcan  6345  ereq1  6366  ereq2  6367  elecg  6397  ereldm  6402  ixpiinm  6548  enfi  6696  creur  8575  eqreznegel  9256  ltxr  9403  icoshftf1o  9615  elfzm11  9712  elfzomelpfzo  9849  nn0ennn  10047  nnesq  10252  rexfiuz  10601  cau4  10728  sumeq2  10967  fisumcom2  11046  dvdsflip  11344  divgcdcoprm0  11575  hashdvds  11689  tpspropd  11985  tgss2  12030  lmbr2  12164  txcnmpt  12223  blininf  12352  blres  12362  xmeterval  12363  xmspropd  12405  mspropd  12406  metequiv  12423  limcdifap  12512  cbvrald  12576  bj-dcbi  12707