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  1550  drnf1  1744  drnf2  1745  drsb1  1810  sbal2  2032  eubidh  2044  eubid  2045  mobidh  2072  mobid  2073  eqeq1  2196  eqeq2  2199  eleq1w  2250  eleq2w  2251  eleq1  2252  eleq2  2253  cbvabw  2312  eqabdv  2318  nfceqdf  2331  drnfc1  2349  drnfc2  2350  neeq1  2373  neeq2  2374  neleq1  2459  neleq2  2460  dfrex2dc  2481  ralbida  2484  rexbida  2485  ralbidv2  2492  rexbidv2  2493  ralbid2  2494  rexbid2  2495  r19.21t  2565  r19.23t  2597  reubida  2672  rmobida  2677  raleqf  2682  rexeqf  2683  reueq1f  2684  rmoeq1f  2685  cbvraldva2  2725  cbvrexdva2  2726  dfsbcq  2979  sbceqbid  2984  sbcbi2  3028  sbcbid  3035  eqsbc2  3038  sbcabel  3059  sbnfc2  3132  ssconb  3283  uneq1  3297  ineq1  3344  difin2  3412  reuun2  3433  reldisj  3489  undif4  3500  disjssun  3501  sbcssg  3547  eltpg  3652  raltpg  3660  rextpg  3661  r19.12sn  3673  opeq1  3793  opeq2  3794  intmin4  3887  dfiun2g  3933  iindif2m  3969  iinin2m  3970  breq  4020  breq1  4021  breq2  4022  treq  4122  opthg2  4257  poeq1  4317  soeq1  4333  frforeq1  4361  freq1  4362  frforeq2  4363  freq2  4364  frforeq3  4365  weeq1  4374  weeq2  4375  ordeq  4390  limeq  4395  rabxfrd  4487  iunpw  4498  opthprc  4695  releq  4726  sbcrel  4730  eqrel  4733  eqrelrel  4745  xpiindim  4782  brcnvg  4826  brresg  4933  resieq  4935  xpcanm  5086  xpcan2m  5087  dmsnopg  5118  dfco2a  5147  cnvpom  5189  cnvsom  5190  iotaeq  5204  sniota  5226  sbcfung  5259  fneq1  5323  fneq2  5324  feq1  5367  feq2  5368  feq3  5369  sbcfng  5382  sbcfg  5383  f1eq1  5435  f1eq2  5436  f1eq3  5437  foeq1  5453  foeq2  5454  foeq3  5455  f1oeq1  5468  f1oeq2  5469  f1oeq3  5470  fun11iun  5501  mpteqb  5627  dffo3  5684  fmptco  5703  dff13  5790  f1imaeq  5797  f1eqcocnv  5813  fliftcnv  5817  isoeq1  5823  isoeq2  5824  isoeq3  5825  isoeq4  5826  isoeq5  5827  isocnv2  5834  acexmid  5895  fnotovb  5939  mpoeq123  5955  ottposg  6280  dmtpos  6281  smoeq  6315  nnacan  6537  nnmcan  6544  ereq1  6566  ereq2  6567  elecg  6599  ereldm  6604  ixpiinm  6750  enfi  6901  elfi2  7001  fipwssg  7008  ctssdccl  7140  tapeq1  7281  tapeq2  7282  creur  8946  eqreznegel  9644  ltxr  9805  icoshftf1o  10021  elfzm11  10121  elfzomelpfzo  10261  nn0ennn  10464  nnesq  10671  rexfiuz  11030  cau4  11157  sumeq2  11399  fisumcom2  11478  fprodcom2fi  11666  dvdsflip  11889  divgcdcoprm0  12133  hashdvds  12253  4sqlem12  12434  imasaddfnlemg  12791  issgrpv  12867  issgrpn0  12868  mndpropd  12901  ismhm  12913  mhmpropd  12918  issubm2  12925  grppropd  12962  grpinvcnv  13012  conjghm  13215  conjnmzb  13219  ghmpropd  13222  cmnpropd  13234  ablpropd  13235  eqgabl  13267  rngpropd  13309  issrg  13319  ringpropd  13392  crngpropd  13393  subrngpropd  13563  subrgpropd  13595  lmodprop2d  13664  islssm  13673  islssmg  13674  lsspropdg  13747  df2idl2rng  13823  tpspropd  13996  tgss2  14039  lmbr2  14174  txcnmpt  14233  txhmeo  14279  blininf  14384  blres  14394  xmeterval  14395  xmspropd  14437  mspropd  14438  metequiv  14455  xmetxpbl  14468  limcdifap  14591  cbvrald  15001  bj-indeq  15142