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  796  stbid  837  dcbid  843  pm4.14dc  895  orbididc  959  ifpbi123d  998  3orbi123d  1345  3anbi123d  1346  xorbi2d  1422  xorbi1d  1423  nfbidf  1585  drnf1  1779  drnf2  1780  drsb1  1845  sbal2  2071  eubidh  2083  eubid  2084  mobidh  2111  mobid  2112  eqeq1  2236  eqeq2  2239  eleq1w  2290  eleq2w  2291  eleq1  2292  eleq2  2293  cbvabw  2352  eqabdv  2358  nfceqdf  2371  drnfc1  2389  drnfc2  2390  neeq1  2413  neeq2  2414  neleq1  2499  neleq2  2500  dfrex2dc  2521  ralbida  2524  rexbida  2525  ralbidv2  2532  rexbidv2  2533  ralbid2  2534  rexbid2  2535  r19.21t  2605  r19.23t  2638  reubida  2713  rmobida  2719  raleqf  2724  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  cbvraldva2  2772  cbvrexdva2  2773  dfsbcq  3030  sbceqbid  3035  sbcbi2  3079  sbcbid  3086  eqsbc2  3089  sbcabel  3111  sbnfc2  3185  ssconb  3337  uneq1  3351  ineq1  3398  difin2  3466  reuun2  3487  reldisj  3543  undif4  3554  disjssun  3555  sbcssg  3600  eltpg  3711  raltpg  3719  rextpg  3720  r19.12sn  3732  opeq1  3857  opeq2  3858  intmin4  3951  dfiun2g  3997  iindif2m  4033  iinin2m  4034  breq  4085  breq1  4086  breq2  4087  treq  4188  opthg2  4325  poeq1  4390  soeq1  4406  frforeq1  4434  freq1  4435  frforeq2  4436  freq2  4437  frforeq3  4438  weeq1  4447  weeq2  4448  ordeq  4463  limeq  4468  rabxfrd  4560  iunpw  4571  opthprc  4770  releq  4801  sbcrel  4805  eqrel  4808  eqrelrel  4820  xpiindim  4859  brcnvg  4903  brresg  5013  resieq  5015  xpcanm  5168  xpcan2m  5169  dmsnopg  5200  dfco2a  5229  cnvpom  5271  cnvsom  5272  iotaeq  5287  sniota  5309  sbcfung  5342  fneq1  5409  fneq2  5410  feq1  5456  feq2  5457  feq3  5458  sbcfng  5471  sbcfg  5472  f1eq1  5528  f1eq2  5529  f1eq3  5530  foeq1  5546  foeq2  5547  foeq3  5548  f1oeq1  5562  f1oeq2  5563  f1oeq3  5564  fun11iun  5595  mpteqb  5727  dffo3  5784  fmptco  5803  dff13  5898  f1imaeq  5905  f1eqcocnv  5921  fliftcnv  5925  isoeq1  5931  isoeq2  5932  isoeq3  5933  isoeq4  5934  isoeq5  5935  isocnv2  5942  acexmid  6006  fnotovb  6053  mpoeq123  6069  ottposg  6407  dmtpos  6408  smoeq  6442  nnacan  6666  nnmcan  6673  ereq1  6695  ereq2  6696  elecg  6728  ereldm  6733  ixpiinm  6879  enfi  7043  elfi2  7150  fipwssg  7157  ctssdccl  7289  tapeq1  7449  tapeq2  7450  creur  9117  eqreznegel  9821  ltxr  9983  icoshftf1o  10199  elfzm11  10299  elfzomelpfzo  10449  nn0ennn  10667  nnesq  10893  rexfiuz  11516  cau4  11643  sumeq2  11886  fisumcom2  11965  fprodcom2fi  12153  dvdsflip  12378  bitsmod  12483  bitscmp  12485  divgcdcoprm0  12639  hashdvds  12759  4sqlem12  12941  imasaddfnlemg  13363  issgrpv  13453  issgrpn0  13454  mndpropd  13489  ismhm  13510  mhmpropd  13515  issubm2  13522  grppropd  13566  grpinvcnv  13617  conjghm  13829  conjnmzb  13833  ghmpropd  13836  cmnpropd  13848  ablpropd  13849  eqgabl  13883  rngpropd  13934  issrg  13944  ringpropd  14017  crngpropd  14018  opprnzrbg  14165  subrngpropd  14196  resrhm2b  14229  subrgpropd  14233  rhmpropd  14234  opprdomnbg  14254  lmodprop2d  14328  islssm  14337  islssmg  14338  lsspropdg  14411  df2idl2rng  14488  tpspropd  14726  tgss2  14769  lmbr2  14904  txcnmpt  14963  txhmeo  15009  blininf  15114  blres  15124  xmeterval  15125  xmspropd  15167  mspropd  15168  metequiv  15185  xmetxpbl  15198  limcdifap  15352  lgsquadlem1  15772  lgsquadlem2  15773  ushgredgedg  16040  ushgredgedgloop  16042  upgriswlkdc  16106  cbvrald  16235  bj-indeq  16375