Theorem 3bitr4g 223

Description: More general version of 3bitr4i 212. 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	bitrid 192	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	bitr4di 198	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> 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:  bibi1d  233  pm5.32rd  451  orbi1d  792  stbid  833  dcbid  839  pm4.14dc  891  orbididc  955  3orbi123d  1322  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  nfbidf  1553  drnf1  1747  drnf2  1748  drsb1  1813  sbal2  2039  eubidh  2051  eubid  2052  mobidh  2079  mobid  2080  eqeq1  2203  eqeq2  2206  eleq1w  2257  eleq2w  2258  eleq1  2259  eleq2  2260  cbvabw  2319  eqabdv  2325  nfceqdf  2338  drnfc1  2356  drnfc2  2357  neeq1  2380  neeq2  2381  neleq1  2466  neleq2  2467  dfrex2dc  2488  ralbida  2491  rexbida  2492  ralbidv2  2499  rexbidv2  2500  ralbid2  2501  rexbid2  2502  r19.21t  2572  r19.23t  2604  reubida  2679  rmobida  2684  raleqf  2689  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  cbvraldva2  2736  cbvrexdva2  2737  dfsbcq  2991  sbceqbid  2996  sbcbi2  3040  sbcbid  3047  eqsbc2  3050  sbcabel  3071  sbnfc2  3145  ssconb  3296  uneq1  3310  ineq1  3357  difin2  3425  reuun2  3446  reldisj  3502  undif4  3513  disjssun  3514  sbcssg  3559  eltpg  3667  raltpg  3675  rextpg  3676  r19.12sn  3688  opeq1  3808  opeq2  3809  intmin4  3902  dfiun2g  3948  iindif2m  3984  iinin2m  3985  breq  4035  breq1  4036  breq2  4037  treq  4137  opthg2  4272  poeq1  4334  soeq1  4350  frforeq1  4378  freq1  4379  frforeq2  4380  freq2  4381  frforeq3  4382  weeq1  4391  weeq2  4392  ordeq  4407  limeq  4412  rabxfrd  4504  iunpw  4515  opthprc  4714  releq  4745  sbcrel  4749  eqrel  4752  eqrelrel  4764  xpiindim  4803  brcnvg  4847  brresg  4954  resieq  4956  xpcanm  5109  xpcan2m  5110  dmsnopg  5141  dfco2a  5170  cnvpom  5212  cnvsom  5213  iotaeq  5227  sniota  5249  sbcfung  5282  fneq1  5346  fneq2  5347  feq1  5390  feq2  5391  feq3  5392  sbcfng  5405  sbcfg  5406  f1eq1  5458  f1eq2  5459  f1eq3  5460  foeq1  5476  foeq2  5477  foeq3  5478  f1oeq1  5492  f1oeq2  5493  f1oeq3  5494  fun11iun  5525  mpteqb  5652  dffo3  5709  fmptco  5728  dff13  5815  f1imaeq  5822  f1eqcocnv  5838  fliftcnv  5842  isoeq1  5848  isoeq2  5849  isoeq3  5850  isoeq4  5851  isoeq5  5852  isocnv2  5859  acexmid  5921  fnotovb  5965  mpoeq123  5981  ottposg  6313  dmtpos  6314  smoeq  6348  nnacan  6570  nnmcan  6577  ereq1  6599  ereq2  6600  elecg  6632  ereldm  6637  ixpiinm  6783  enfi  6934  elfi2  7038  fipwssg  7045  ctssdccl  7177  tapeq1  7319  tapeq2  7320  creur  8986  eqreznegel  9688  ltxr  9850  icoshftf1o  10066  elfzm11  10166  elfzomelpfzo  10307  nn0ennn  10525  nnesq  10751  rexfiuz  11154  cau4  11281  sumeq2  11524  fisumcom2  11603  fprodcom2fi  11791  dvdsflip  12016  divgcdcoprm0  12269  hashdvds  12389  4sqlem12  12571  imasaddfnlemg  12957  issgrpv  13047  issgrpn0  13048  mndpropd  13081  ismhm  13093  mhmpropd  13098  issubm2  13105  grppropd  13149  grpinvcnv  13200  conjghm  13406  conjnmzb  13410  ghmpropd  13413  cmnpropd  13425  ablpropd  13426  eqgabl  13460  rngpropd  13511  issrg  13521  ringpropd  13594  crngpropd  13595  opprnzrbg  13741  subrngpropd  13772  resrhm2b  13805  subrgpropd  13809  rhmpropd  13810  opprdomnbg  13830  lmodprop2d  13904  islssm  13913  islssmg  13914  lsspropdg  13987  df2idl2rng  14064  tpspropd  14272  tgss2  14315  lmbr2  14450  txcnmpt  14509  txhmeo  14555  blininf  14660  blres  14670  xmeterval  14671  xmspropd  14713  mspropd  14714  metequiv  14731  xmetxpbl  14744  limcdifap  14898  lgsquadlem1  15318  lgsquadlem2  15319  cbvrald  15434  bj-indeq  15575