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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1d  233  pm5.32rd  455  orbi1d  803  stbid  844  dcbid  850  pm4.14dc  902  orbididc  966  ifpbi123d  1005  3orbi123d  1352  3anbi123d  1353  xorbi2d  1429  xorbi1d  1430  nfbidf  1592  drnf1  1786  drnf2  1787  drsb1  1852  sbal2  2080  eubidh  2092  eubid  2093  mobidh  2120  mobid  2121  eqeq1  2245  eqeq2  2248  eleq1w  2299  eleq2w  2300  eleq1  2301  eleq2  2302  abbi  2357  cbvabw  2363  eqabdv  2369  nfceqdf  2391  drnfc1  2409  drnfc2  2410  neeq1  2433  neeq2  2434  neleq1  2519  neleq2  2520  dfrex2dc  2541  ralbida  2544  rexbida  2545  ralbidv2  2552  rexbidv2  2553  ralbid2  2554  rexbid2  2555  r19.21t  2625  r19.23t  2658  reubida  2734  rmobida  2740  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  cbvraldva2  2793  cbvrexdva2  2794  dfsbcq  3053  sbceqbid  3058  sbcbi2  3102  sbcbid  3109  eqsbc2  3112  sbcabel  3134  sbnfc2  3208  ssconb  3362  uneq1  3376  ineq1  3425  difin2  3493  reuun2  3516  reldisj  3576  undif4  3587  disjssun  3588  sbcssg  3636  eltpg  3754  raltpg  3762  rextpg  3763  r19.12sn  3775  opeq1  3904  opeq2  3905  intmin4  3998  dfiun2g  4044  iindif2m  4080  iinin2m  4081  breq  4133  breq1  4134  breq2  4135  treq  4237  opthg2  4381  poeq1  4446  soeq1  4462  frforeq1  4490  freq1  4491  frforeq2  4492  freq2  4493  frforeq3  4494  weeq1  4503  weeq2  4504  ordeq  4519  limeq  4524  rabxfrd  4617  iunpw  4628  opthprc  4828  releq  4859  sbcrel  4863  eqrel  4866  eqrelrel  4878  xpiindim  4919  brcnvg  4963  brresg  5073  resieq  5075  xpcanm  5230  xpcan2m  5231  dmsnopg  5262  dfco2a  5291  cnvpom  5333  cnvsom  5334  iotaeq  5349  sniota  5371  sbcfung  5404  fneq1  5472  fneq2  5473  feq1  5519  feq2  5520  feq3  5521  sbcfng  5534  sbcfg  5535  f1eq1  5596  f1eq2  5597  f1eq3  5598  foeq1  5614  foeq2  5615  foeq3  5616  f1oeq1  5630  f1oeq2  5631  f1oeq3  5632  fun11iun  5663  mpteqb  5799  dffo3  5858  fmptco  5877  dff13  5977  f1imaeq  5984  f1eqcocnv  6000  fliftcnv  6004  isoeq1  6010  isoeq2  6011  isoeq3  6012  isoeq4  6013  isoeq5  6014  isocnv2  6021  acexmid  6087  fnotovb  6134  mpoeq123  6150  ottposg  6531  dmtpos  6532  smoeq  6566  nnacan  6790  nnmcan  6797  ereq1  6819  ereq2  6820  elecg  6852  ereldm  6857  ixpiinm  7012  enfi  7181  elfi2  7311  fipwssg  7318  ctssdccl  7457  papeq1  7615  papeq2  7616  tapeq1  7624  tapeq2  7625  creur  9297  eqreznegel  10029  ltxr  10193  icoshftf1o  10409  elfzm11  10514  elfzomelpfzo  10665  nn0ennn  10890  nnesq  11117  hashf1lem1  11306  rexfiuz  11776  cau4  11904  sumeq2  12149  fisumcom2  12229  fprodcom2fi  12417  dvdsflip  12642  bitsmod  12747  bitscmp  12749  divgcdcoprm0  12903  hashdvds  13027  4sqlem12  13209  imasaddfnlemg  13693  issgrpv  13777  issgrpn0  13778  mndpropd  13811  ismhm  13826  mhmpropd  13831  issubm2  13838  grppropd  13880  grpinvcnv  13931  conjghm  14137  conjnmzb  14141  ghmpropd  14144  cmnpropd  14187  ablpropd  14188  eqgabl  14223  gsumcom2fi  14274  rngpropd  14360  issrg  14375  ringpropd  14449  crngpropd  14450  opprnzrbg  14600  opprlring  14612  subrngpropd  14632  resrhm2b  14665  subrgpropd  14669  rhmpropd  14670  opprdomnbg  14691  opprdrng  14728  lmodprop2d  14793  islssm  14802  islssmg  14803  lsspropdg  14876  df2idl2rng  14953  assapropd  15122  psrbagconf1o  15177  tpspropd  15279  tgss2  15322  lmbr2  15457  txcnmpt  15516  txhmeo  15562  blininf  15667  blres  15677  xmeterval  15678  xmspropd  15720  mspropd  15721  metequiv  15738  xmetxpbl  15751  limcdifap  15905  lgsquadlem1  16418  lgsquadlem2  16419  ushgredgedg  16689  ushgredgedgloop  16691  upgriswlkdc  16823  clwwlknonel  16895  eupth2lem2dc  16922  cbvrald  17038  bj-indeq  17177  alsbid  17367