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  740  stbid  777  dcbid  786  pm4.14dc  825  orbididc  899  3orbi123d  1247  3anbi123d  1248  xorbi2d  1316  xorbi1d  1317  nfbidf  1477  drnf1  1668  drnf2  1669  drsb1  1727  sbal2  1946  eubidh  1954  eubid  1955  mobidh  1982  mobid  1983  eqeq1  2094  eqeq2  2097  eleq1w  2148  eleq2w  2149  eleq1  2150  eleq2  2151  nfceqdf  2227  drnfc1  2245  drnfc2  2246  neeq1  2268  neeq2  2269  neleq1  2354  neleq2  2355  dfrex2dc  2371  ralbida  2374  rexbida  2375  ralbidv2  2382  rexbidv2  2383  r19.21t  2448  r19.23t  2479  reubida  2548  rmobida  2553  raleqf  2558  rexeqf  2559  reueq1f  2560  rmoeq1f  2561  cbvraldva2  2594  cbvrexdva2  2595  dfsbcq  2840  sbcbi2  2887  sbcbid  2894  eqsbc3r  2897  sbcabel  2918  sbnfc2  2986  ssconb  3131  uneq1  3145  ineq1  3192  difin2  3259  reuun2  3280  reldisj  3331  undif4  3342  disjssun  3343  sbcssg  3387  eltpg  3483  raltpg  3490  rextpg  3491  r19.12sn  3503  opeq1  3617  opeq2  3618  intmin4  3711  dfiun2g  3757  iindif2m  3792  iinin2m  3793  breq  3839  breq1  3840  breq2  3841  treq  3934  opthg2  4057  poeq1  4117  soeq1  4133  frforeq1  4161  freq1  4162  frforeq2  4163  freq2  4164  frforeq3  4165  weeq1  4174  weeq2  4175  ordeq  4190  limeq  4195  rabxfrd  4282  iunpw  4292  opthprc  4477  releq  4508  sbcrel  4512  eqrel  4515  eqrelrel  4527  xpiindim  4561  brcnvg  4605  brresg  4709  resieq  4711  xpcanm  4857  xpcan2m  4858  dmsnopg  4889  dfco2a  4918  cnvpom  4960  cnvsom  4961  iotaeq  4975  sniota  4994  sbcfung  5025  fneq1  5088  fneq2  5089  feq1  5131  feq2  5132  feq3  5133  sbcfng  5145  sbcfg  5146  f1eq1  5195  f1eq2  5196  f1eq3  5197  foeq1  5213  foeq2  5214  foeq3  5215  f1oeq1  5228  f1oeq2  5229  f1oeq3  5230  fun11iun  5258  mpteqb  5377  dffo3  5430  fmptco  5448  dff13  5529  f1imaeq  5536  f1eqcocnv  5552  fliftcnv  5556  isoeq1  5562  isoeq2  5563  isoeq3  5564  isoeq4  5565  isoeq5  5566  isocnv2  5573  acexmid  5633  fnotovb  5674  mpt2eq123  5690  ottposg  6002  dmtpos  6003  smoeq  6037  nnacan  6251  nnmcan  6258  ereq1  6279  ereq2  6280  elecg  6310  ereldm  6315  enfi  6569  creur  8391  eqreznegel  9068  ltxr  9215  icoshftf1o  9377  elfzm11  9472  elfzomelpfzo  9607  nn0ennn  9805  nnesq  10037  rexfiuz  10386  cau4  10513  sumeq2  10711  fisumcom2  10793  dvdsflip  10932  divgcdcoprm0  11163  hashdvds  11277  cbvrald  11332  bj-dcbi  11463