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  5526  f1eq2  5527  f1eq3  5528  foeq1  5544  foeq2  5545  foeq3  5546  f1oeq1  5560  f1oeq2  5561  f1oeq3  5562  fun11iun  5593  mpteqb  5725  dffo3  5782  fmptco  5801  dff13  5892  f1imaeq  5899  f1eqcocnv  5915  fliftcnv  5919  isoeq1  5925  isoeq2  5926  isoeq3  5927  isoeq4  5928  isoeq5  5929  isocnv2  5936  acexmid  6000  fnotovb  6047  mpoeq123  6063  ottposg  6401  dmtpos  6402  smoeq  6436  nnacan  6658  nnmcan  6665  ereq1  6687  ereq2  6688  elecg  6720  ereldm  6725  ixpiinm  6871  enfi  7035  elfi2  7139  fipwssg  7146  ctssdccl  7278  tapeq1  7438  tapeq2  7439  creur  9106  eqreznegel  9809  ltxr  9971  icoshftf1o  10187  elfzm11  10287  elfzomelpfzo  10437  nn0ennn  10655  nnesq  10881  rexfiuz  11500  cau4  11627  sumeq2  11870  fisumcom2  11949  fprodcom2fi  12137  dvdsflip  12362  bitsmod  12467  bitscmp  12469  divgcdcoprm0  12623  hashdvds  12743  4sqlem12  12925  imasaddfnlemg  13347  issgrpv  13437  issgrpn0  13438  mndpropd  13473  ismhm  13494  mhmpropd  13499  issubm2  13506  grppropd  13550  grpinvcnv  13601  conjghm  13813  conjnmzb  13817  ghmpropd  13820  cmnpropd  13832  ablpropd  13833  eqgabl  13867  rngpropd  13918  issrg  13928  ringpropd  14001  crngpropd  14002  opprnzrbg  14149  subrngpropd  14180  resrhm2b  14213  subrgpropd  14217  rhmpropd  14218  opprdomnbg  14238  lmodprop2d  14312  islssm  14321  islssmg  14322  lsspropdg  14395  df2idl2rng  14472  tpspropd  14710  tgss2  14753  lmbr2  14888  txcnmpt  14947  txhmeo  14993  blininf  15098  blres  15108  xmeterval  15109  xmspropd  15151  mspropd  15152  metequiv  15169  xmetxpbl  15182  limcdifap  15336  lgsquadlem1  15756  lgsquadlem2  15757  ushgredgedg  16024  ushgredgedgloop  16026  upgriswlkdc  16071  cbvrald  16152  bj-indeq  16292