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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1d  233  pm5.32rd  455  orbi1d  803  stbid  844  dcbid  850  pm4.14dc  902  orbididc  966  ifpbi123d  1005  3orbi123d  1352  3anbi123d  1353  xorbi2d  1429  xorbi1d  1430  nfbidf  1592  drnf1  1786  drnf2  1787  drsb1  1852  sbal2  2080  eubidh  2092  eubid  2093  mobidh  2120  mobid  2121  eqeq1  2245  eqeq2  2248  eleq1w  2299  eleq2w  2300  eleq1  2301  eleq2  2302  abbi  2357  cbvabw  2363  eqabdv  2369  nfceqdf  2391  drnfc1  2409  drnfc2  2410  neeq1  2433  neeq2  2434  neleq1  2519  neleq2  2520  dfrex2dc  2541  ralbida  2544  rexbida  2545  ralbidv2  2552  rexbidv2  2553  ralbid2  2554  rexbid2  2555  r19.21t  2625  r19.23t  2658  reubida  2734  rmobida  2740  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  cbvraldva2  2793  cbvrexdva2  2794  dfsbcq  3053  sbceqbid  3058  sbcbi2  3102  sbcbid  3109  eqsbc2  3112  sbcabel  3134  sbnfc2  3208  ssconb  3362  uneq1  3376  ineq1  3425  difin2  3493  reuun2  3516  reldisj  3576  undif4  3587  disjssun  3588  sbcssg  3636  eltpg  3754  raltpg  3762  rextpg  3763  r19.12sn  3775  opeq1  3904  opeq2  3905  intmin4  3998  dfiun2g  4044  iindif2m  4080  iinin2m  4081  breq  4133  breq1  4134  breq2  4135  treq  4237  opthg2  4381  poeq1  4446  soeq1  4462  frforeq1  4490  freq1  4491  frforeq2  4492  freq2  4493  frforeq3  4494  weeq1  4503  weeq2  4504  ordeq  4519  limeq  4524  rabxfrd  4617  iunpw  4628  opthprc  4828  releq  4859  sbcrel  4863  eqrel  4866  eqrelrel  4878  xpiindim  4919  brcnvg  4963  brresg  5073  resieq  5075  xpcanm  5230  xpcan2m  5231  dmsnopg  5262  dfco2a  5291  cnvpom  5333  cnvsom  5334  iotaeq  5349  sniota  5371  sbcfung  5404  fneq1  5472  fneq2  5473  feq1  5519  feq2  5520  feq3  5521  sbcfng  5534  sbcfg  5535  f1eq1  5596  f1eq2  5597  f1eq3  5598  foeq1  5614  foeq2  5615  foeq3  5616  f1oeq1  5630  f1oeq2  5631  f1oeq3  5632  fun11iun  5663  mpteqb  5799  dffo3  5858  fmptco  5877  dff13  5977  f1imaeq  5984  f1eqcocnv  6000  fliftcnv  6004  isoeq1  6010  isoeq2  6011  isoeq3  6012  isoeq4  6013  isoeq5  6014  isocnv2  6021  acexmid  6087  fnotovb  6134  mpoeq123  6150  ottposg  6530  dmtpos  6531  smoeq  6565  nnacan  6789  nnmcan  6796  ereq1  6818  ereq2  6819  elecg  6851  ereldm  6856  ixpiinm  7010  enfi  7179  elfi2  7311  fipwssg  7318  ctssdccl  7457  papeq1  7615  papeq2  7616  tapeq1  7624  tapeq2  7625  creur  9297  eqreznegel  10030  ltxr  10194  icoshftf1o  10410  elfzm11  10515  elfzomelpfzo  10666  nn0ennn  10891  nnesq  11118  hashf1lem1  11307  rexfiuz  11777  cau4  11905  sumeq2  12150  fisumcom2  12230  fprodcom2fi  12418  dvdsflip  12643  bitsmod  12748  bitscmp  12750  divgcdcoprm0  12904  hashdvds  13028  4sqlem12  13210  imasaddfnlemg  13694  issgrpv  13778  issgrpn0  13779  mndpropd  13812  ismhm  13827  mhmpropd  13832  issubm2  13839  grppropd  13881  grpinvcnv  13932  conjghm  14138  conjnmzb  14142  ghmpropd  14145  cmnpropd  14188  ablpropd  14189  eqgabl  14224  gsumcom2fi  14275  rngpropd  14361  issrg  14376  ringpropd  14450  crngpropd  14451  opprnzrbg  14601  opprlring  14613  subrngpropd  14633  resrhm2b  14666  subrgpropd  14670  rhmpropd  14671  opprdomnbg  14692  opprdrng  14729  lmodprop2d  14794  islssm  14803  islssmg  14804  lsspropdg  14877  df2idl2rng  14954  assapropd  15123  psrbagconf1o  15174  tpspropd  15262  tgss2  15305  lmbr2  15440  txcnmpt  15499  txhmeo  15545  blininf  15650  blres  15660  xmeterval  15661  xmspropd  15703  mspropd  15704  metequiv  15721  xmetxpbl  15734  limcdifap  15888  lgsquadlem1  16401  lgsquadlem2  16402  ushgredgedg  16672  ushgredgedgloop  16674  upgriswlkdc  16806  clwwlknonel  16878  eupth2lem2dc  16905  cbvrald  17021  bj-indeq  17160  alsbid  17350