Theorem 3bitr4g 212

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bibi1d  222  pm5.32rd  424  orbi1d  705  dcbid  748  pm4.14dc  787  orbididc  860  3orbi123d  1206  3anbi123d  1207  xorbi2d  1271  xorbi1d  1272  nfbidf  1432  drnf1  1621  drnf2  1622  drsb1  1680  sbal2  1898  eubidh  1906  eubid  1907  mobidh  1934  mobid  1935  eqeq1  2046  eqeq2  2049  eleq1  2100  eleq2  2101  nfceqdf  2177  drnfc1  2194  drnfc2  2195  neeq1  2218  neeq2  2219  neleq1  2301  neleq2  2302  ralbida  2320  rexbida  2321  ralbidv2  2328  rexbidv2  2329  r19.21t  2394  r19.23t  2423  reubida  2491  rmobida  2496  raleqf  2501  rexeqf  2502  reueq1f  2503  rmoeq1f  2504  cbvraldva2  2537  cbvrexdva2  2538  dfsbcq  2766  sbcbid  2816  sbcabel  2839  sbnfc2  2906  psseq1  3031  psseq2  3032  ssconb  3076  uneq1  3090  ineq1  3131  difin2  3199  reuun2  3220  reldisj  3271  undif4  3284  disjssun  3285  sbcssg  3330  eltpg  3416  raltpg  3423  rextpg  3424  opeq1  3549  opeq2  3550  intmin4  3643  dfiun2g  3689  iindif2m  3724  iinin2m  3725  breq  3766  breq1  3767  breq2  3768  treq  3860  opthg2  3976  poeq1  4036  soeq1  4052  frforeq1  4080  freq1  4081  frforeq2  4082  freq2  4083  frforeq3  4084  weeq1  4093  weeq2  4094  ordeq  4109  limeq  4114  rabxfrd  4201  iunpw  4211  opthprc  4391  releq  4422  sbcrel  4426  eqrel  4429  eqrelrel  4441  xpiindim  4473  brcnvg  4516  brresg  4620  resieq  4622  xpcanm  4760  xpcan2m  4761  dmsnopg  4792  dfco2a  4821  cnvpom  4860  cnvsom  4861  iotaeq  4875  sniota  4894  sbcfung  4925  fneq1  4987  fneq2  4988  feq1  5030  feq2  5031  feq3  5032  sbcfng  5044  sbcfg  5045  f1eq1  5087  f1eq2  5088  f1eq3  5089  foeq1  5102  foeq2  5103  foeq3  5104  f1oeq1  5117  f1oeq2  5118  f1oeq3  5119  fun11iun  5147  mpteqb  5261  dffo3  5314  fmptco  5330  dff13  5407  f1imaeq  5414  f1imapss  5415  f1eqcocnv  5431  fliftcnv  5435  isoeq1  5441  isoeq2  5442  isoeq3  5443  isoeq4  5444  isoeq5  5445  isocnv2  5452  acexmid  5511  fnotovb  5548  mpt2eq123  5564  ottposg  5870  dmtpos  5871  smoeq  5905  nnacan  6085  nnmcan  6092  ereq1  6113  ereq2  6114  elecg  6144  ereldm  6149  enfi  6334  creur  7911  eqreznegel  8549  ltxr  8695  icoshftf1o  8859  elfzm11  8953  elfzomelpfzo  9087  nn0ennn  9209  nnesq  9368  cau4  9712  cbvrald  9927  bj-dcbi  10048