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  793  stbid  834  dcbid  840  pm4.14dc  892  orbididc  956  3orbi123d  1324  3anbi123d  1325  xorbi2d  1400  xorbi1d  1401  nfbidf  1562  drnf1  1756  drnf2  1757  drsb1  1822  sbal2  2048  eubidh  2060  eubid  2061  mobidh  2088  mobid  2089  eqeq1  2212  eqeq2  2215  eleq1w  2266  eleq2w  2267  eleq1  2268  eleq2  2269  cbvabw  2328  eqabdv  2334  nfceqdf  2347  drnfc1  2365  drnfc2  2366  neeq1  2389  neeq2  2390  neleq1  2475  neleq2  2476  dfrex2dc  2497  ralbida  2500  rexbida  2501  ralbidv2  2508  rexbidv2  2509  ralbid2  2510  rexbid2  2511  r19.21t  2581  r19.23t  2613  reubida  2688  rmobida  2693  raleqf  2698  rexeqf  2699  reueq1f  2700  rmoeq1f  2701  cbvraldva2  2745  cbvrexdva2  2746  dfsbcq  3000  sbceqbid  3005  sbcbi2  3049  sbcbid  3056  eqsbc2  3059  sbcabel  3080  sbnfc2  3154  ssconb  3306  uneq1  3320  ineq1  3367  difin2  3435  reuun2  3456  reldisj  3512  undif4  3523  disjssun  3524  sbcssg  3569  eltpg  3678  raltpg  3686  rextpg  3687  r19.12sn  3699  opeq1  3819  opeq2  3820  intmin4  3913  dfiun2g  3959  iindif2m  3995  iinin2m  3996  breq  4047  breq1  4048  breq2  4049  treq  4149  opthg2  4284  poeq1  4347  soeq1  4363  frforeq1  4391  freq1  4392  frforeq2  4393  freq2  4394  frforeq3  4395  weeq1  4404  weeq2  4405  ordeq  4420  limeq  4425  rabxfrd  4517  iunpw  4528  opthprc  4727  releq  4758  sbcrel  4762  eqrel  4765  eqrelrel  4777  xpiindim  4816  brcnvg  4860  brresg  4968  resieq  4970  xpcanm  5123  xpcan2m  5124  dmsnopg  5155  dfco2a  5184  cnvpom  5226  cnvsom  5227  iotaeq  5241  sniota  5263  sbcfung  5296  fneq1  5363  fneq2  5364  feq1  5410  feq2  5411  feq3  5412  sbcfng  5425  sbcfg  5426  f1eq1  5478  f1eq2  5479  f1eq3  5480  foeq1  5496  foeq2  5497  foeq3  5498  f1oeq1  5512  f1oeq2  5513  f1oeq3  5514  fun11iun  5545  mpteqb  5672  dffo3  5729  fmptco  5748  dff13  5839  f1imaeq  5846  f1eqcocnv  5862  fliftcnv  5866  isoeq1  5872  isoeq2  5873  isoeq3  5874  isoeq4  5875  isoeq5  5876  isocnv2  5883  acexmid  5945  fnotovb  5990  mpoeq123  6006  ottposg  6343  dmtpos  6344  smoeq  6378  nnacan  6600  nnmcan  6607  ereq1  6629  ereq2  6630  elecg  6662  ereldm  6667  ixpiinm  6813  enfi  6972  elfi2  7076  fipwssg  7083  ctssdccl  7215  tapeq1  7366  tapeq2  7367  creur  9034  eqreznegel  9737  ltxr  9899  icoshftf1o  10115  elfzm11  10215  elfzomelpfzo  10362  nn0ennn  10580  nnesq  10806  rexfiuz  11333  cau4  11460  sumeq2  11703  fisumcom2  11782  fprodcom2fi  11970  dvdsflip  12195  bitsmod  12300  bitscmp  12302  divgcdcoprm0  12456  hashdvds  12576  4sqlem12  12758  imasaddfnlemg  13179  issgrpv  13269  issgrpn0  13270  mndpropd  13305  ismhm  13326  mhmpropd  13331  issubm2  13338  grppropd  13382  grpinvcnv  13433  conjghm  13645  conjnmzb  13649  ghmpropd  13652  cmnpropd  13664  ablpropd  13665  eqgabl  13699  rngpropd  13750  issrg  13760  ringpropd  13833  crngpropd  13834  opprnzrbg  13980  subrngpropd  14011  resrhm2b  14044  subrgpropd  14048  rhmpropd  14049  opprdomnbg  14069  lmodprop2d  14143  islssm  14152  islssmg  14153  lsspropdg  14226  df2idl2rng  14303  tpspropd  14541  tgss2  14584  lmbr2  14719  txcnmpt  14778  txhmeo  14824  blininf  14929  blres  14939  xmeterval  14940  xmspropd  14982  mspropd  14983  metequiv  15000  xmetxpbl  15013  limcdifap  15167  lgsquadlem1  15587  lgsquadlem2  15588  cbvrald  15761  bj-indeq  15902