Theorem 3bitr4g 222

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1d  232  pm5.32rd  446  orbi1d  780  stbid  817  dcbid  823  pm4.14dc  875  orbididc  937  3orbi123d  1289  3anbi123d  1290  xorbi2d  1358  xorbi1d  1359  nfbidf  1519  drnf1  1711  drnf2  1712  drsb1  1771  sbal2  1997  eubidh  2005  eubid  2006  mobidh  2033  mobid  2034  eqeq1  2146  eqeq2  2149  eleq1w  2200  eleq2w  2201  eleq1  2202  eleq2  2203  nfceqdf  2280  drnfc1  2298  drnfc2  2299  neeq1  2321  neeq2  2322  neleq1  2407  neleq2  2408  dfrex2dc  2428  ralbida  2431  rexbida  2432  ralbidv2  2439  rexbidv2  2440  r19.21t  2507  r19.23t  2539  reubida  2612  rmobida  2617  raleqf  2622  rexeqf  2623  reueq1f  2624  rmoeq1f  2625  cbvraldva2  2661  cbvrexdva2  2662  dfsbcq  2911  sbcbi2  2959  sbcbid  2966  eqsbc3r  2969  sbcabel  2990  sbnfc2  3060  ssconb  3209  uneq1  3223  ineq1  3270  difin2  3338  reuun2  3359  reldisj  3414  undif4  3425  disjssun  3426  sbcssg  3472  eltpg  3569  raltpg  3576  rextpg  3577  r19.12sn  3589  opeq1  3705  opeq2  3706  intmin4  3799  dfiun2g  3845  iindif2m  3880  iinin2m  3881  breq  3931  breq1  3932  breq2  3933  treq  4032  opthg2  4161  poeq1  4221  soeq1  4237  frforeq1  4265  freq1  4266  frforeq2  4267  freq2  4268  frforeq3  4269  weeq1  4278  weeq2  4279  ordeq  4294  limeq  4299  rabxfrd  4390  iunpw  4401  opthprc  4590  releq  4621  sbcrel  4625  eqrel  4628  eqrelrel  4640  xpiindim  4676  brcnvg  4720  brresg  4827  resieq  4829  xpcanm  4978  xpcan2m  4979  dmsnopg  5010  dfco2a  5039  cnvpom  5081  cnvsom  5082  iotaeq  5096  sniota  5115  sbcfung  5147  fneq1  5211  fneq2  5212  feq1  5255  feq2  5256  feq3  5257  sbcfng  5270  sbcfg  5271  f1eq1  5323  f1eq2  5324  f1eq3  5325  foeq1  5341  foeq2  5342  foeq3  5343  f1oeq1  5356  f1oeq2  5357  f1oeq3  5358  fun11iun  5388  mpteqb  5511  dffo3  5567  fmptco  5586  dff13  5669  f1imaeq  5676  f1eqcocnv  5692  fliftcnv  5696  isoeq1  5702  isoeq2  5703  isoeq3  5704  isoeq4  5705  isoeq5  5706  isocnv2  5713  acexmid  5773  fnotovb  5814  mpoeq123  5830  ottposg  6152  dmtpos  6153  smoeq  6187  nnacan  6408  nnmcan  6415  ereq1  6436  ereq2  6437  elecg  6467  ereldm  6472  ixpiinm  6618  enfi  6767  elfi2  6860  fipwssg  6867  ctssdccl  6996  creur  8717  eqreznegel  9406  ltxr  9562  icoshftf1o  9774  elfzm11  9871  elfzomelpfzo  10008  nn0ennn  10206  nnesq  10411  rexfiuz  10761  cau4  10888  sumeq2  11128  fisumcom2  11207  dvdsflip  11549  divgcdcoprm0  11782  hashdvds  11897  tpspropd  12203  tgss2  12248  lmbr2  12383  txcnmpt  12442  txhmeo  12488  blininf  12593  blres  12603  xmeterval  12604  xmspropd  12646  mspropd  12647  metequiv  12664  xmetxpbl  12677  limcdifap  12800  cbvrald  12995