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  799  stbid  840  dcbid  846  pm4.14dc  898  orbididc  962  ifpbi123d  1001  3orbi123d  1348  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  nfbidf  1588  drnf1  1782  drnf2  1783  drsb1  1848  sbal2  2074  eubidh  2086  eubid  2087  mobidh  2114  mobid  2115  eqeq1  2239  eqeq2  2242  eleq1w  2293  eleq2w  2294  eleq1  2295  eleq2  2296  abbi  2351  cbvabw  2357  eqabdv  2363  nfceqdf  2383  drnfc1  2401  drnfc2  2402  neeq1  2425  neeq2  2426  neleq1  2511  neleq2  2512  dfrex2dc  2533  ralbida  2536  rexbida  2537  ralbidv2  2544  rexbidv2  2545  ralbid2  2546  rexbid2  2547  r19.21t  2617  r19.23t  2650  reubida  2725  rmobida  2731  raleqf  2736  rexeqf  2737  reueq1f  2738  rmoeq1f  2739  cbvraldva2  2784  cbvrexdva2  2785  dfsbcq  3043  sbceqbid  3048  sbcbi2  3092  sbcbid  3099  eqsbc2  3102  sbcabel  3124  sbnfc2  3198  ssconb  3351  uneq1  3365  ineq1  3414  difin2  3482  reuun2  3503  reldisj  3559  undif4  3570  disjssun  3571  sbcssg  3617  eltpg  3733  raltpg  3741  rextpg  3742  r19.12sn  3754  opeq1  3882  opeq2  3883  intmin4  3976  dfiun2g  4022  iindif2m  4058  iinin2m  4059  breq  4110  breq1  4111  breq2  4112  treq  4213  opthg2  4354  poeq1  4419  soeq1  4435  frforeq1  4463  freq1  4464  frforeq2  4465  freq2  4466  frforeq3  4467  weeq1  4476  weeq2  4477  ordeq  4492  limeq  4497  rabxfrd  4589  iunpw  4600  opthprc  4800  releq  4831  sbcrel  4835  eqrel  4838  eqrelrel  4850  xpiindim  4891  brcnvg  4935  brresg  5045  resieq  5047  xpcanm  5201  xpcan2m  5202  dmsnopg  5233  dfco2a  5262  cnvpom  5304  cnvsom  5305  iotaeq  5320  sniota  5342  sbcfung  5375  fneq1  5443  fneq2  5444  feq1  5490  feq2  5491  feq3  5492  sbcfng  5505  sbcfg  5506  f1eq1  5567  f1eq2  5568  f1eq3  5569  foeq1  5585  foeq2  5586  foeq3  5587  f1oeq1  5601  f1oeq2  5602  f1oeq3  5603  fun11iun  5634  mpteqb  5767  dffo3  5823  fmptco  5842  dff13  5940  f1imaeq  5947  f1eqcocnv  5963  fliftcnv  5967  isoeq1  5973  isoeq2  5974  isoeq3  5975  isoeq4  5976  isoeq5  5977  isocnv2  5984  acexmid  6048  fnotovb  6095  mpoeq123  6111  ottposg  6485  dmtpos  6486  smoeq  6520  nnacan  6744  nnmcan  6751  ereq1  6773  ereq2  6774  elecg  6806  ereldm  6811  ixpiinm  6958  enfi  7127  elfi2  7258  fipwssg  7265  ctssdccl  7401  tapeq1  7565  tapeq2  7566  creur  9232  eqreznegel  9945  ltxr  10107  icoshftf1o  10323  elfzm11  10424  elfzomelpfzo  10575  nn0ennn  10794  nnesq  11020  rexfiuz  11670  cau4  11797  sumeq2  12040  fisumcom2  12120  fprodcom2fi  12308  dvdsflip  12533  bitsmod  12638  bitscmp  12640  divgcdcoprm0  12794  hashdvds  12914  4sqlem12  13096  imasaddfnlemg  13519  issgrpv  13609  issgrpn0  13610  mndpropd  13645  ismhm  13666  mhmpropd  13671  issubm2  13678  grppropd  13722  grpinvcnv  13773  conjghm  13985  conjnmzb  13989  ghmpropd  13992  cmnpropd  14004  ablpropd  14005  eqgabl  14039  rngpropd  14091  issrg  14101  ringpropd  14174  crngpropd  14175  opprnzrbg  14322  subrngpropd  14353  resrhm2b  14386  subrgpropd  14390  rhmpropd  14391  opprdomnbg  14412  lmodprop2d  14488  islssm  14497  islssmg  14498  lsspropdg  14571  df2idl2rng  14648  psrbagconf1o  14820  tpspropd  14893  tgss2  14936  lmbr2  15071  txcnmpt  15130  txhmeo  15176  blininf  15281  blres  15291  xmeterval  15292  xmspropd  15334  mspropd  15335  metequiv  15352  xmetxpbl  15365  limcdifap  15519  lgsquadlem1  15942  lgsquadlem2  15943  ushgredgedg  16213  ushgredgedgloop  16215  upgriswlkdc  16347  clwwlknonel  16419  eupth2lem2dc  16446  cbvrald  16552  bj-indeq  16691