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  793  stbid  834  dcbid  840  pm4.14dc  892  orbididc  956  3orbi123d  1324  3anbi123d  1325  xorbi2d  1400  xorbi1d  1401  nfbidf  1563  drnf1  1757  drnf2  1758  drsb1  1823  sbal2  2049  eubidh  2061  eubid  2062  mobidh  2089  mobid  2090  eqeq1  2213  eqeq2  2216  eleq1w  2267  eleq2w  2268  eleq1  2269  eleq2  2270  cbvabw  2329  eqabdv  2335  nfceqdf  2348  drnfc1  2366  drnfc2  2367  neeq1  2390  neeq2  2391  neleq1  2476  neleq2  2477  dfrex2dc  2498  ralbida  2501  rexbida  2502  ralbidv2  2509  rexbidv2  2510  ralbid2  2511  rexbid2  2512  r19.21t  2582  r19.23t  2614  reubida  2689  rmobida  2694  raleqf  2699  rexeqf  2700  reueq1f  2701  rmoeq1f  2702  cbvraldva2  2746  cbvrexdva2  2747  dfsbcq  3004  sbceqbid  3009  sbcbi2  3053  sbcbid  3060  eqsbc2  3063  sbcabel  3084  sbnfc2  3158  ssconb  3310  uneq1  3324  ineq1  3371  difin2  3439  reuun2  3460  reldisj  3516  undif4  3527  disjssun  3528  sbcssg  3573  eltpg  3683  raltpg  3691  rextpg  3692  r19.12sn  3704  opeq1  3825  opeq2  3826  intmin4  3919  dfiun2g  3965  iindif2m  4001  iinin2m  4002  breq  4053  breq1  4054  breq2  4055  treq  4156  opthg2  4291  poeq1  4354  soeq1  4370  frforeq1  4398  freq1  4399  frforeq2  4400  freq2  4401  frforeq3  4402  weeq1  4411  weeq2  4412  ordeq  4427  limeq  4432  rabxfrd  4524  iunpw  4535  opthprc  4734  releq  4765  sbcrel  4769  eqrel  4772  eqrelrel  4784  xpiindim  4823  brcnvg  4867  brresg  4976  resieq  4978  xpcanm  5131  xpcan2m  5132  dmsnopg  5163  dfco2a  5192  cnvpom  5234  cnvsom  5235  iotaeq  5249  sniota  5271  sbcfung  5304  fneq1  5371  fneq2  5372  feq1  5418  feq2  5419  feq3  5420  sbcfng  5433  sbcfg  5434  f1eq1  5488  f1eq2  5489  f1eq3  5490  foeq1  5506  foeq2  5507  foeq3  5508  f1oeq1  5522  f1oeq2  5523  f1oeq3  5524  fun11iun  5555  mpteqb  5683  dffo3  5740  fmptco  5759  dff13  5850  f1imaeq  5857  f1eqcocnv  5873  fliftcnv  5877  isoeq1  5883  isoeq2  5884  isoeq3  5885  isoeq4  5886  isoeq5  5887  isocnv2  5894  acexmid  5956  fnotovb  6001  mpoeq123  6017  ottposg  6354  dmtpos  6355  smoeq  6389  nnacan  6611  nnmcan  6618  ereq1  6640  ereq2  6641  elecg  6673  ereldm  6678  ixpiinm  6824  enfi  6985  elfi2  7089  fipwssg  7096  ctssdccl  7228  tapeq1  7384  tapeq2  7385  creur  9052  eqreznegel  9755  ltxr  9917  icoshftf1o  10133  elfzm11  10233  elfzomelpfzo  10382  nn0ennn  10600  nnesq  10826  rexfiuz  11375  cau4  11502  sumeq2  11745  fisumcom2  11824  fprodcom2fi  12012  dvdsflip  12237  bitsmod  12342  bitscmp  12344  divgcdcoprm0  12498  hashdvds  12618  4sqlem12  12800  imasaddfnlemg  13221  issgrpv  13311  issgrpn0  13312  mndpropd  13347  ismhm  13368  mhmpropd  13373  issubm2  13380  grppropd  13424  grpinvcnv  13475  conjghm  13687  conjnmzb  13691  ghmpropd  13694  cmnpropd  13706  ablpropd  13707  eqgabl  13741  rngpropd  13792  issrg  13802  ringpropd  13875  crngpropd  13876  opprnzrbg  14022  subrngpropd  14053  resrhm2b  14086  subrgpropd  14090  rhmpropd  14091  opprdomnbg  14111  lmodprop2d  14185  islssm  14194  islssmg  14195  lsspropdg  14268  df2idl2rng  14345  tpspropd  14583  tgss2  14626  lmbr2  14761  txcnmpt  14820  txhmeo  14866  blininf  14971  blres  14981  xmeterval  14982  xmspropd  15024  mspropd  15025  metequiv  15042  xmetxpbl  15055  limcdifap  15209  lgsquadlem1  15629  lgsquadlem2  15630  cbvrald  15863  bj-indeq  16003