Theorem 3bitr4g 221

Description: More general version of 3bitr4i 210. 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	syl5bb 190	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 196	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi1d  231  pm5.32rd  439  orbi1d  738  dcbid  782  pm4.14dc  821  orbididc  895  3orbi123d  1243  3anbi123d  1244  xorbi2d  1312  xorbi1d  1313  nfbidf  1473  drnf1  1662  drnf2  1663  drsb1  1721  sbal2  1940  eubidh  1948  eubid  1949  mobidh  1976  mobid  1977  eqeq1  2088  eqeq2  2091  eleq1  2142  eleq2  2143  nfceqdf  2219  drnfc1  2236  drnfc2  2237  neeq1  2259  neeq2  2260  neleq1  2344  neleq2  2345  ralbida  2363  rexbida  2364  ralbidv2  2371  rexbidv2  2372  r19.21t  2437  r19.23t  2468  reubida  2536  rmobida  2541  raleqf  2546  rexeqf  2547  reueq1f  2548  rmoeq1f  2549  cbvraldva2  2582  cbvrexdva2  2583  dfsbcq  2818  sbcbi2  2865  sbcbid  2872  eqsbc3r  2875  sbcabel  2896  sbnfc2  2963  ssconb  3106  uneq1  3120  ineq1  3167  difin2  3233  reuun2  3254  reldisj  3302  undif4  3313  disjssun  3314  sbcssg  3358  eltpg  3446  raltpg  3453  rextpg  3454  r19.12sn  3466  opeq1  3578  opeq2  3579  intmin4  3672  dfiun2g  3718  iindif2m  3753  iinin2m  3754  breq  3795  breq1  3796  breq2  3797  treq  3889  opthg2  4002  poeq1  4062  soeq1  4078  frforeq1  4106  freq1  4107  frforeq2  4108  freq2  4109  frforeq3  4110  weeq1  4119  weeq2  4120  ordeq  4135  limeq  4140  rabxfrd  4227  iunpw  4237  opthprc  4417  releq  4448  sbcrel  4452  eqrel  4455  eqrelrel  4467  xpiindim  4501  brcnvg  4544  brresg  4648  resieq  4650  xpcanm  4790  xpcan2m  4791  dmsnopg  4822  dfco2a  4851  cnvpom  4890  cnvsom  4891  iotaeq  4905  sniota  4924  sbcfung  4955  fneq1  5018  fneq2  5019  feq1  5061  feq2  5062  feq3  5063  sbcfng  5075  sbcfg  5076  f1eq1  5118  f1eq2  5119  f1eq3  5120  foeq1  5133  foeq2  5134  foeq3  5135  f1oeq1  5148  f1oeq2  5149  f1oeq3  5150  fun11iun  5178  mpteqb  5293  dffo3  5346  fmptco  5362  dff13  5439  f1imaeq  5446  f1eqcocnv  5462  fliftcnv  5466  isoeq1  5472  isoeq2  5473  isoeq3  5474  isoeq4  5475  isoeq5  5476  isocnv2  5483  acexmid  5542  fnotovb  5579  mpt2eq123  5595  ottposg  5904  dmtpos  5905  smoeq  5939  nnacan  6151  nnmcan  6158  ereq1  6179  ereq2  6180  elecg  6210  ereldm  6215  enfi  6408  creur  8103  eqreznegel  8780  ltxr  8927  icoshftf1o  9089  elfzm11  9184  elfzomelpfzo  9317  nn0ennn  9515  nnesq  9689  rexfiuz  10013  cau4  10140  sumeq2d  10334  sumeq2  10335  dvdsflip  10396  divgcdcoprm0  10627  cbvrald  10749  bj-dcbi  10877