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  791  stbid  832  dcbid  838  pm4.14dc  890  orbididc  953  3orbi123d  1311  3anbi123d  1312  xorbi2d  1380  xorbi1d  1381  nfbidf  1539  drnf1  1733  drnf2  1734  drsb1  1799  sbal2  2020  eubidh  2032  eubid  2033  mobidh  2060  mobid  2061  eqeq1  2184  eqeq2  2187  eleq1w  2238  eleq2w  2239  eleq1  2240  eleq2  2241  cbvabw  2300  nfceqdf  2318  drnfc1  2336  drnfc2  2337  neeq1  2360  neeq2  2361  neleq1  2446  neleq2  2447  dfrex2dc  2468  ralbida  2471  rexbida  2472  ralbidv2  2479  rexbidv2  2480  ralbid2  2481  rexbid2  2482  r19.21t  2552  r19.23t  2584  reubida  2658  rmobida  2663  raleqf  2668  rexeqf  2669  reueq1f  2670  rmoeq1f  2671  cbvraldva2  2710  cbvrexdva2  2711  dfsbcq  2964  sbceqbid  2969  sbcbi2  3013  sbcbid  3020  eqsbc2  3023  sbcabel  3044  sbnfc2  3117  ssconb  3268  uneq1  3282  ineq1  3329  difin2  3397  reuun2  3418  reldisj  3474  undif4  3485  disjssun  3486  sbcssg  3532  eltpg  3637  raltpg  3645  rextpg  3646  r19.12sn  3658  opeq1  3778  opeq2  3779  intmin4  3872  dfiun2g  3918  iindif2m  3954  iinin2m  3955  breq  4005  breq1  4006  breq2  4007  treq  4107  opthg2  4239  poeq1  4299  soeq1  4315  frforeq1  4343  freq1  4344  frforeq2  4345  freq2  4346  frforeq3  4347  weeq1  4356  weeq2  4357  ordeq  4372  limeq  4377  rabxfrd  4469  iunpw  4480  opthprc  4677  releq  4708  sbcrel  4712  eqrel  4715  eqrelrel  4727  xpiindim  4764  brcnvg  4808  brresg  4915  resieq  4917  xpcanm  5068  xpcan2m  5069  dmsnopg  5100  dfco2a  5129  cnvpom  5171  cnvsom  5172  iotaeq  5186  sniota  5207  sbcfung  5240  fneq1  5304  fneq2  5305  feq1  5348  feq2  5349  feq3  5350  sbcfng  5363  sbcfg  5364  f1eq1  5416  f1eq2  5417  f1eq3  5418  foeq1  5434  foeq2  5435  foeq3  5436  f1oeq1  5449  f1oeq2  5450  f1oeq3  5451  fun11iun  5482  mpteqb  5606  dffo3  5663  fmptco  5682  dff13  5768  f1imaeq  5775  f1eqcocnv  5791  fliftcnv  5795  isoeq1  5801  isoeq2  5802  isoeq3  5803  isoeq4  5804  isoeq5  5805  isocnv2  5812  acexmid  5873  fnotovb  5917  mpoeq123  5933  ottposg  6255  dmtpos  6256  smoeq  6290  nnacan  6512  nnmcan  6519  ereq1  6541  ereq2  6542  elecg  6572  ereldm  6577  ixpiinm  6723  enfi  6872  elfi2  6970  fipwssg  6977  ctssdccl  7109  tapeq1  7250  tapeq2  7251  creur  8915  eqreznegel  9613  ltxr  9774  icoshftf1o  9990  elfzm11  10090  elfzomelpfzo  10230  nn0ennn  10432  nnesq  10639  rexfiuz  10997  cau4  11124  sumeq2  11366  fisumcom2  11445  fprodcom2fi  11633  dvdsflip  11856  divgcdcoprm0  12100  hashdvds  12220  imasaddfnlemg  12734  issgrpv  12809  issgrpn0  12810  mndpropd  12840  ismhm  12852  mhmpropd  12856  issubm2  12863  grppropd  12892  grpinvcnv  12937  cmnpropd  13096  ablpropd  13097  issrg  13146  ringpropd  13215  crngpropd  13216  subrgpropd  13367  tpspropd  13506  tgss2  13549  lmbr2  13684  txcnmpt  13743  txhmeo  13789  blininf  13894  blres  13904  xmeterval  13905  xmspropd  13947  mspropd  13948  metequiv  13965  xmetxpbl  13978  limcdifap  14101  cbvrald  14510  bj-indeq  14651