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  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  3575  undif4  3586  disjssun  3587  sbcssg  3633  eltpg  3750  raltpg  3758  rextpg  3759  r19.12sn  3771  opeq1  3899  opeq2  3900  intmin4  3993  dfiun2g  4039  iindif2m  4075  iinin2m  4076  breq  4127  breq1  4128  breq2  4129  treq  4230  opthg2  4374  poeq1  4439  soeq1  4455  frforeq1  4483  freq1  4484  frforeq2  4485  freq2  4486  frforeq3  4487  weeq1  4496  weeq2  4497  ordeq  4512  limeq  4517  rabxfrd  4610  iunpw  4621  opthprc  4821  releq  4852  sbcrel  4856  eqrel  4859  eqrelrel  4871  xpiindim  4912  brcnvg  4956  brresg  5066  resieq  5068  xpcanm  5222  xpcan2m  5223  dmsnopg  5254  dfco2a  5283  cnvpom  5325  cnvsom  5326  iotaeq  5341  sniota  5363  sbcfung  5396  fneq1  5464  fneq2  5465  feq1  5511  feq2  5512  feq3  5513  sbcfng  5526  sbcfg  5527  f1eq1  5588  f1eq2  5589  f1eq3  5590  foeq1  5606  foeq2  5607  foeq3  5608  f1oeq1  5622  f1oeq2  5623  f1oeq3  5624  fun11iun  5655  mpteqb  5790  dffo3  5846  fmptco  5865  dff13  5964  f1imaeq  5971  f1eqcocnv  5987  fliftcnv  5991  isoeq1  5997  isoeq2  5998  isoeq3  5999  isoeq4  6000  isoeq5  6001  isocnv2  6008  acexmid  6074  fnotovb  6121  mpoeq123  6137  ottposg  6516  dmtpos  6517  smoeq  6551  nnacan  6775  nnmcan  6782  ereq1  6804  ereq2  6805  elecg  6837  ereldm  6842  ixpiinm  6996  enfi  7165  elfi2  7296  fipwssg  7303  ctssdccl  7441  papeq1  7599  papeq2  7600  tapeq1  7608  tapeq2  7609  creur  9279  eqreznegel  9993  ltxr  10156  icoshftf1o  10372  elfzm11  10476  elfzomelpfzo  10627  nn0ennn  10848  nnesq  11075  hashf1lem1  11263  rexfiuz  11733  cau4  11860  sumeq2  12103  fisumcom2  12183  fprodcom2fi  12371  dvdsflip  12596  bitsmod  12701  bitscmp  12703  divgcdcoprm0  12857  hashdvds  12977  4sqlem12  13159  imasaddfnlemg  13612  issgrpv  13696  issgrpn0  13697  mndpropd  13730  ismhm  13745  mhmpropd  13750  issubm2  13757  grppropd  13799  grpinvcnv  13850  conjghm  14056  conjnmzb  14060  ghmpropd  14063  cmnpropd  14075  ablpropd  14076  eqgabl  14111  rngpropd  14229  issrg  14243  ringpropd  14316  crngpropd  14317  opprnzrbg  14465  opprlring  14477  subrngpropd  14497  resrhm2b  14530  subrgpropd  14534  rhmpropd  14535  opprdomnbg  14556  opprdrng  14593  lmodprop2d  14657  islssm  14666  islssmg  14667  lsspropdg  14740  df2idl2rng  14817  psrbagconf1o  14987  tpspropd  15060  tgss2  15103  lmbr2  15238  txcnmpt  15297  txhmeo  15343  blininf  15448  blres  15458  xmeterval  15459  xmspropd  15501  mspropd  15502  metequiv  15519  xmetxpbl  15532  limcdifap  15686  lgsquadlem1  16110  lgsquadlem2  16111  ushgredgedg  16381  ushgredgedgloop  16383  upgriswlkdc  16515  clwwlknonel  16587  eupth2lem2dc  16614  cbvrald  16730  bj-indeq  16869