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  799  stbid  840  dcbid  846  pm4.14dc  898  orbididc  962  ifpbi123d  1001  3orbi123d  1348  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  nfbidf  1588  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  2355  eqabdv  2361  nfceqdf  2374  drnfc1  2392  drnfc2  2393  neeq1  2416  neeq2  2417  neleq1  2502  neleq2  2503  dfrex2dc  2524  ralbida  2527  rexbida  2528  ralbidv2  2535  rexbidv2  2536  ralbid2  2537  rexbid2  2538  r19.21t  2608  r19.23t  2641  reubida  2716  rmobida  2722  raleqf  2727  rexeqf  2728  reueq1f  2729  rmoeq1f  2730  cbvraldva2  2775  cbvrexdva2  2776  dfsbcq  3034  sbceqbid  3039  sbcbi2  3083  sbcbid  3090  eqsbc2  3093  sbcabel  3115  sbnfc2  3189  ssconb  3342  uneq1  3356  ineq1  3403  difin2  3471  reuun2  3492  reldisj  3548  undif4  3559  disjssun  3560  sbcssg  3605  eltpg  3718  raltpg  3726  rextpg  3727  r19.12sn  3739  opeq1  3867  opeq2  3868  intmin4  3961  dfiun2g  4007  iindif2m  4043  iinin2m  4044  breq  4095  breq1  4096  breq2  4097  treq  4198  opthg2  4337  poeq1  4402  soeq1  4418  frforeq1  4446  freq1  4447  frforeq2  4448  freq2  4449  frforeq3  4450  weeq1  4459  weeq2  4460  ordeq  4475  limeq  4480  rabxfrd  4572  iunpw  4583  opthprc  4783  releq  4814  sbcrel  4818  eqrel  4821  eqrelrel  4833  xpiindim  4873  brcnvg  4917  brresg  5027  resieq  5029  xpcanm  5183  xpcan2m  5184  dmsnopg  5215  dfco2a  5244  cnvpom  5286  cnvsom  5287  iotaeq  5302  sniota  5324  sbcfung  5357  fneq1  5425  fneq2  5426  feq1  5472  feq2  5473  feq3  5474  sbcfng  5487  sbcfg  5488  f1eq1  5546  f1eq2  5547  f1eq3  5548  foeq1  5564  foeq2  5565  foeq3  5566  f1oeq1  5580  f1oeq2  5581  f1oeq3  5582  fun11iun  5613  mpteqb  5746  dffo3  5802  fmptco  5821  dff13  5919  f1imaeq  5926  f1eqcocnv  5942  fliftcnv  5946  isoeq1  5952  isoeq2  5953  isoeq3  5954  isoeq4  5955  isoeq5  5956  isocnv2  5963  acexmid  6027  fnotovb  6074  mpoeq123  6090  ottposg  6464  dmtpos  6465  smoeq  6499  nnacan  6723  nnmcan  6730  ereq1  6752  ereq2  6753  elecg  6785  ereldm  6790  ixpiinm  6936  enfi  7103  elfi2  7231  fipwssg  7238  ctssdccl  7370  tapeq1  7531  tapeq2  7532  creur  9198  eqreznegel  9909  ltxr  10071  icoshftf1o  10287  elfzm11  10388  elfzomelpfzo  10539  nn0ennn  10758  nnesq  10984  rexfiuz  11629  cau4  11756  sumeq2  11999  fisumcom2  12079  fprodcom2fi  12267  dvdsflip  12492  bitsmod  12597  bitscmp  12599  divgcdcoprm0  12753  hashdvds  12873  4sqlem12  13055  imasaddfnlemg  13477  issgrpv  13567  issgrpn0  13568  mndpropd  13603  ismhm  13624  mhmpropd  13629  issubm2  13636  grppropd  13680  grpinvcnv  13731  conjghm  13943  conjnmzb  13947  ghmpropd  13950  cmnpropd  13962  ablpropd  13963  eqgabl  13997  rngpropd  14049  issrg  14059  ringpropd  14132  crngpropd  14133  opprnzrbg  14280  subrngpropd  14311  resrhm2b  14344  subrgpropd  14348  rhmpropd  14349  opprdomnbg  14370  lmodprop2d  14444  islssm  14453  islssmg  14454  lsspropdg  14527  df2idl2rng  14604  psrbagconf1o  14774  tpspropd  14847  tgss2  14890  lmbr2  15025  txcnmpt  15084  txhmeo  15130  blininf  15235  blres  15245  xmeterval  15246  xmspropd  15288  mspropd  15289  metequiv  15306  xmetxpbl  15319  limcdifap  15473  lgsquadlem1  15896  lgsquadlem2  15897  ushgredgedg  16167  ushgredgedgloop  16169  upgriswlkdc  16301  clwwlknonel  16373  eupth2lem2dc  16400  cbvrald  16506  bj-indeq  16645