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  798  stbid  839  dcbid  845  pm4.14dc  897  orbididc  961  ifpbi123d  1000  3orbi123d  1347  3anbi123d  1348  xorbi2d  1424  xorbi1d  1425  nfbidf  1587  drnf1  1781  drnf2  1782  drsb1  1847  sbal2  2073  eubidh  2085  eubid  2086  mobidh  2113  mobid  2114  eqeq1  2238  eqeq2  2241  eleq1w  2292  eleq2w  2293  eleq1  2294  eleq2  2295  cbvabw  2354  eqabdv  2360  nfceqdf  2373  drnfc1  2391  drnfc2  2392  neeq1  2415  neeq2  2416  neleq1  2501  neleq2  2502  dfrex2dc  2523  ralbida  2526  rexbida  2527  ralbidv2  2534  rexbidv2  2535  ralbid2  2536  rexbid2  2537  r19.21t  2607  r19.23t  2640  reubida  2715  rmobida  2721  raleqf  2726  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  cbvraldva2  2774  cbvrexdva2  2775  dfsbcq  3033  sbceqbid  3038  sbcbi2  3082  sbcbid  3089  eqsbc2  3092  sbcabel  3114  sbnfc2  3188  ssconb  3340  uneq1  3354  ineq1  3401  difin2  3469  reuun2  3490  reldisj  3546  undif4  3557  disjssun  3558  sbcssg  3603  eltpg  3714  raltpg  3722  rextpg  3723  r19.12sn  3735  opeq1  3862  opeq2  3863  intmin4  3956  dfiun2g  4002  iindif2m  4038  iinin2m  4039  breq  4090  breq1  4091  breq2  4092  treq  4193  opthg2  4331  poeq1  4396  soeq1  4412  frforeq1  4440  freq1  4441  frforeq2  4442  freq2  4443  frforeq3  4444  weeq1  4453  weeq2  4454  ordeq  4469  limeq  4474  rabxfrd  4566  iunpw  4577  opthprc  4777  releq  4808  sbcrel  4812  eqrel  4815  eqrelrel  4827  xpiindim  4867  brcnvg  4911  brresg  5021  resieq  5023  xpcanm  5176  xpcan2m  5177  dmsnopg  5208  dfco2a  5237  cnvpom  5279  cnvsom  5280  iotaeq  5295  sniota  5317  sbcfung  5350  fneq1  5418  fneq2  5419  feq1  5465  feq2  5466  feq3  5467  sbcfng  5480  sbcfg  5481  f1eq1  5537  f1eq2  5538  f1eq3  5539  foeq1  5555  foeq2  5556  foeq3  5557  f1oeq1  5571  f1oeq2  5572  f1oeq3  5573  fun11iun  5604  mpteqb  5737  dffo3  5794  fmptco  5813  dff13  5909  f1imaeq  5916  f1eqcocnv  5932  fliftcnv  5936  isoeq1  5942  isoeq2  5943  isoeq3  5944  isoeq4  5945  isoeq5  5946  isocnv2  5953  acexmid  6017  fnotovb  6064  mpoeq123  6080  ottposg  6421  dmtpos  6422  smoeq  6456  nnacan  6680  nnmcan  6687  ereq1  6709  ereq2  6710  elecg  6742  ereldm  6747  ixpiinm  6893  enfi  7060  elfi2  7171  fipwssg  7178  ctssdccl  7310  tapeq1  7471  tapeq2  7472  creur  9139  eqreznegel  9848  ltxr  10010  icoshftf1o  10226  elfzm11  10326  elfzomelpfzo  10477  nn0ennn  10696  nnesq  10922  rexfiuz  11567  cau4  11694  sumeq2  11937  fisumcom2  12017  fprodcom2fi  12205  dvdsflip  12430  bitsmod  12535  bitscmp  12537  divgcdcoprm0  12691  hashdvds  12811  4sqlem12  12993  imasaddfnlemg  13415  issgrpv  13505  issgrpn0  13506  mndpropd  13541  ismhm  13562  mhmpropd  13567  issubm2  13574  grppropd  13618  grpinvcnv  13669  conjghm  13881  conjnmzb  13885  ghmpropd  13888  cmnpropd  13900  ablpropd  13901  eqgabl  13935  rngpropd  13987  issrg  13997  ringpropd  14070  crngpropd  14071  opprnzrbg  14218  subrngpropd  14249  resrhm2b  14282  subrgpropd  14286  rhmpropd  14287  opprdomnbg  14307  lmodprop2d  14381  islssm  14390  islssmg  14391  lsspropdg  14464  df2idl2rng  14541  tpspropd  14779  tgss2  14822  lmbr2  14957  txcnmpt  15016  txhmeo  15062  blininf  15167  blres  15177  xmeterval  15178  xmspropd  15220  mspropd  15221  metequiv  15238  xmetxpbl  15251  limcdifap  15405  lgsquadlem1  15825  lgsquadlem2  15826  ushgredgedg  16096  ushgredgedgloop  16098  upgriswlkdc  16230  clwwlknonel  16302  eupth2lem2dc  16329  cbvrald  16435  bj-indeq  16575