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  793  stbid  834  dcbid  840  pm4.14dc  892  orbididc  956  3orbi123d  1324  3anbi123d  1325  xorbi2d  1400  xorbi1d  1401  nfbidf  1563  drnf1  1757  drnf2  1758  drsb1  1823  sbal2  2049  eubidh  2061  eubid  2062  mobidh  2089  mobid  2090  eqeq1  2214  eqeq2  2217  eleq1w  2268  eleq2w  2269  eleq1  2270  eleq2  2271  cbvabw  2330  eqabdv  2336  nfceqdf  2349  drnfc1  2367  drnfc2  2368  neeq1  2391  neeq2  2392  neleq1  2477  neleq2  2478  dfrex2dc  2499  ralbida  2502  rexbida  2503  ralbidv2  2510  rexbidv2  2511  ralbid2  2512  rexbid2  2513  r19.21t  2583  r19.23t  2615  reubida  2690  rmobida  2696  raleqf  2701  rexeqf  2702  reueq1f  2703  rmoeq1f  2704  cbvraldva2  2749  cbvrexdva2  2750  dfsbcq  3007  sbceqbid  3012  sbcbi2  3056  sbcbid  3063  eqsbc2  3066  sbcabel  3088  sbnfc2  3162  ssconb  3314  uneq1  3328  ineq1  3375  difin2  3443  reuun2  3464  reldisj  3520  undif4  3531  disjssun  3532  sbcssg  3577  eltpg  3688  raltpg  3696  rextpg  3697  r19.12sn  3709  opeq1  3833  opeq2  3834  intmin4  3927  dfiun2g  3973  iindif2m  4009  iinin2m  4010  breq  4061  breq1  4062  breq2  4063  treq  4164  opthg2  4301  poeq1  4364  soeq1  4380  frforeq1  4408  freq1  4409  frforeq2  4410  freq2  4411  frforeq3  4412  weeq1  4421  weeq2  4422  ordeq  4437  limeq  4442  rabxfrd  4534  iunpw  4545  opthprc  4744  releq  4775  sbcrel  4779  eqrel  4782  eqrelrel  4794  xpiindim  4833  brcnvg  4877  brresg  4986  resieq  4988  xpcanm  5141  xpcan2m  5142  dmsnopg  5173  dfco2a  5202  cnvpom  5244  cnvsom  5245  iotaeq  5259  sniota  5281  sbcfung  5314  fneq1  5381  fneq2  5382  feq1  5428  feq2  5429  feq3  5430  sbcfng  5443  sbcfg  5444  f1eq1  5498  f1eq2  5499  f1eq3  5500  foeq1  5516  foeq2  5517  foeq3  5518  f1oeq1  5532  f1oeq2  5533  f1oeq3  5534  fun11iun  5565  mpteqb  5693  dffo3  5750  fmptco  5769  dff13  5860  f1imaeq  5867  f1eqcocnv  5883  fliftcnv  5887  isoeq1  5893  isoeq2  5894  isoeq3  5895  isoeq4  5896  isoeq5  5897  isocnv2  5904  acexmid  5966  fnotovb  6011  mpoeq123  6027  ottposg  6364  dmtpos  6365  smoeq  6399  nnacan  6621  nnmcan  6628  ereq1  6650  ereq2  6651  elecg  6683  ereldm  6688  ixpiinm  6834  enfi  6996  elfi2  7100  fipwssg  7107  ctssdccl  7239  tapeq1  7399  tapeq2  7400  creur  9067  eqreznegel  9770  ltxr  9932  icoshftf1o  10148  elfzm11  10248  elfzomelpfzo  10397  nn0ennn  10615  nnesq  10841  rexfiuz  11415  cau4  11542  sumeq2  11785  fisumcom2  11864  fprodcom2fi  12052  dvdsflip  12277  bitsmod  12382  bitscmp  12384  divgcdcoprm0  12538  hashdvds  12658  4sqlem12  12840  imasaddfnlemg  13261  issgrpv  13351  issgrpn0  13352  mndpropd  13387  ismhm  13408  mhmpropd  13413  issubm2  13420  grppropd  13464  grpinvcnv  13515  conjghm  13727  conjnmzb  13731  ghmpropd  13734  cmnpropd  13746  ablpropd  13747  eqgabl  13781  rngpropd  13832  issrg  13842  ringpropd  13915  crngpropd  13916  opprnzrbg  14062  subrngpropd  14093  resrhm2b  14126  subrgpropd  14130  rhmpropd  14131  opprdomnbg  14151  lmodprop2d  14225  islssm  14234  islssmg  14235  lsspropdg  14308  df2idl2rng  14385  tpspropd  14623  tgss2  14666  lmbr2  14801  txcnmpt  14860  txhmeo  14906  blininf  15011  blres  15021  xmeterval  15022  xmspropd  15064  mspropd  15065  metequiv  15082  xmetxpbl  15095  limcdifap  15249  lgsquadlem1  15669  lgsquadlem2  15670  cbvrald  15924  bj-indeq  16064