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  792  stbid  833  dcbid  839  pm4.14dc  891  orbididc  955  3orbi123d  1322  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  nfbidf  1553  drnf1  1747  drnf2  1748  drsb1  1813  sbal2  2039  eubidh  2051  eubid  2052  mobidh  2079  mobid  2080  eqeq1  2203  eqeq2  2206  eleq1w  2257  eleq2w  2258  eleq1  2259  eleq2  2260  cbvabw  2319  eqabdv  2325  nfceqdf  2338  drnfc1  2356  drnfc2  2357  neeq1  2380  neeq2  2381  neleq1  2466  neleq2  2467  dfrex2dc  2488  ralbida  2491  rexbida  2492  ralbidv2  2499  rexbidv2  2500  ralbid2  2501  rexbid2  2502  r19.21t  2572  r19.23t  2604  reubida  2679  rmobida  2684  raleqf  2689  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  cbvraldva2  2736  cbvrexdva2  2737  dfsbcq  2991  sbceqbid  2996  sbcbi2  3040  sbcbid  3047  eqsbc2  3050  sbcabel  3071  sbnfc2  3145  ssconb  3297  uneq1  3311  ineq1  3358  difin2  3426  reuun2  3447  reldisj  3503  undif4  3514  disjssun  3515  sbcssg  3560  eltpg  3668  raltpg  3676  rextpg  3677  r19.12sn  3689  opeq1  3809  opeq2  3810  intmin4  3903  dfiun2g  3949  iindif2m  3985  iinin2m  3986  breq  4036  breq1  4037  breq2  4038  treq  4138  opthg2  4273  poeq1  4335  soeq1  4351  frforeq1  4379  freq1  4380  frforeq2  4381  freq2  4382  frforeq3  4383  weeq1  4392  weeq2  4393  ordeq  4408  limeq  4413  rabxfrd  4505  iunpw  4516  opthprc  4715  releq  4746  sbcrel  4750  eqrel  4753  eqrelrel  4765  xpiindim  4804  brcnvg  4848  brresg  4955  resieq  4957  xpcanm  5110  xpcan2m  5111  dmsnopg  5142  dfco2a  5171  cnvpom  5213  cnvsom  5214  iotaeq  5228  sniota  5250  sbcfung  5283  fneq1  5347  fneq2  5348  feq1  5393  feq2  5394  feq3  5395  sbcfng  5408  sbcfg  5409  f1eq1  5461  f1eq2  5462  f1eq3  5463  foeq1  5479  foeq2  5480  foeq3  5481  f1oeq1  5495  f1oeq2  5496  f1oeq3  5497  fun11iun  5528  mpteqb  5655  dffo3  5712  fmptco  5731  dff13  5818  f1imaeq  5825  f1eqcocnv  5841  fliftcnv  5845  isoeq1  5851  isoeq2  5852  isoeq3  5853  isoeq4  5854  isoeq5  5855  isocnv2  5862  acexmid  5924  fnotovb  5969  mpoeq123  5985  ottposg  6322  dmtpos  6323  smoeq  6357  nnacan  6579  nnmcan  6586  ereq1  6608  ereq2  6609  elecg  6641  ereldm  6646  ixpiinm  6792  enfi  6943  elfi2  7047  fipwssg  7054  ctssdccl  7186  tapeq1  7335  tapeq2  7336  creur  9003  eqreznegel  9705  ltxr  9867  icoshftf1o  10083  elfzm11  10183  elfzomelpfzo  10324  nn0ennn  10542  nnesq  10768  rexfiuz  11171  cau4  11298  sumeq2  11541  fisumcom2  11620  fprodcom2fi  11808  dvdsflip  12033  bitsmod  12138  bitscmp  12140  divgcdcoprm0  12294  hashdvds  12414  4sqlem12  12596  imasaddfnlemg  13016  issgrpv  13106  issgrpn0  13107  mndpropd  13142  ismhm  13163  mhmpropd  13168  issubm2  13175  grppropd  13219  grpinvcnv  13270  conjghm  13482  conjnmzb  13486  ghmpropd  13489  cmnpropd  13501  ablpropd  13502  eqgabl  13536  rngpropd  13587  issrg  13597  ringpropd  13670  crngpropd  13671  opprnzrbg  13817  subrngpropd  13848  resrhm2b  13881  subrgpropd  13885  rhmpropd  13886  opprdomnbg  13906  lmodprop2d  13980  islssm  13989  islssmg  13990  lsspropdg  14063  df2idl2rng  14140  tpspropd  14356  tgss2  14399  lmbr2  14534  txcnmpt  14593  txhmeo  14639  blininf  14744  blres  14754  xmeterval  14755  xmspropd  14797  mspropd  14798  metequiv  14815  xmetxpbl  14828  limcdifap  14982  lgsquadlem1  15402  lgsquadlem2  15403  cbvrald  15518  bj-indeq  15659