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  4132  breq1  4133  breq2  4134  treq  4235  opthg2  4379  poeq1  4444  soeq1  4460  frforeq1  4488  freq1  4489  frforeq2  4490  freq2  4491  frforeq3  4492  weeq1  4501  weeq2  4502  ordeq  4517  limeq  4522  rabxfrd  4615  iunpw  4626  opthprc  4826  releq  4857  sbcrel  4861  eqrel  4864  eqrelrel  4876  xpiindim  4917  brcnvg  4961  brresg  5071  resieq  5073  xpcanm  5227  xpcan2m  5228  dmsnopg  5259  dfco2a  5288  cnvpom  5330  cnvsom  5331  iotaeq  5346  sniota  5368  sbcfung  5401  fneq1  5469  fneq2  5470  feq1  5516  feq2  5517  feq3  5518  sbcfng  5531  sbcfg  5532  f1eq1  5593  f1eq2  5594  f1eq3  5595  foeq1  5611  foeq2  5612  foeq3  5613  f1oeq1  5627  f1oeq2  5628  f1oeq3  5629  fun11iun  5660  mpteqb  5796  dffo3  5855  fmptco  5874  dff13  5974  f1imaeq  5981  f1eqcocnv  5997  fliftcnv  6001  isoeq1  6007  isoeq2  6008  isoeq3  6009  isoeq4  6010  isoeq5  6011  isocnv2  6018  acexmid  6084  fnotovb  6131  mpoeq123  6147  ottposg  6526  dmtpos  6527  smoeq  6561  nnacan  6785  nnmcan  6792  ereq1  6814  ereq2  6815  elecg  6847  ereldm  6852  ixpiinm  7006  enfi  7175  elfi2  7306  fipwssg  7313  ctssdccl  7452  papeq1  7610  papeq2  7611  tapeq1  7619  tapeq2  7620  creur  9292  eqreznegel  10024  ltxr  10188  icoshftf1o  10404  elfzm11  10509  elfzomelpfzo  10660  nn0ennn  10885  nnesq  11112  hashf1lem1  11301  rexfiuz  11771  cau4  11899  sumeq2  12144  fisumcom2  12224  fprodcom2fi  12412  dvdsflip  12637  bitsmod  12742  bitscmp  12744  divgcdcoprm0  12898  hashdvds  13022  4sqlem12  13204  imasaddfnlemg  13688  issgrpv  13772  issgrpn0  13773  mndpropd  13806  ismhm  13821  mhmpropd  13826  issubm2  13833  grppropd  13875  grpinvcnv  13926  conjghm  14132  conjnmzb  14136  ghmpropd  14139  cmnpropd  14182  ablpropd  14183  eqgabl  14218  rngpropd  14338  issrg  14353  ringpropd  14427  crngpropd  14428  opprnzrbg  14576  opprlring  14588  subrngpropd  14608  resrhm2b  14641  subrgpropd  14645  rhmpropd  14646  opprdomnbg  14667  opprdrng  14704  lmodprop2d  14769  islssm  14778  islssmg  14779  lsspropdg  14852  df2idl2rng  14929  assapropd  15098  psrbagconf1o  15149  tpspropd  15228  tgss2  15271  lmbr2  15406  txcnmpt  15465  txhmeo  15511  blininf  15616  blres  15626  xmeterval  15627  xmspropd  15669  mspropd  15670  metequiv  15687  xmetxpbl  15700  limcdifap  15854  lgsquadlem1  16362  lgsquadlem2  16363  ushgredgedg  16633  ushgredgedgloop  16635  upgriswlkdc  16767  clwwlknonel  16839  eupth2lem2dc  16866  cbvrald  16982  bj-indeq  17121  alsbid  17310