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  799  stbid  840  dcbid  846  pm4.14dc  898  orbididc  962  ifpbi123d  1001  3orbi123d  1348  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  nfbidf  1588  drnf1  1782  drnf2  1783  drsb1  1848  sbal2  2076  eubidh  2088  eubid  2089  mobidh  2116  mobid  2117  eqeq1  2241  eqeq2  2244  eleq1w  2295  eleq2w  2296  eleq1  2297  eleq2  2298  abbi  2353  cbvabw  2359  eqabdv  2365  nfceqdf  2385  drnfc1  2403  drnfc2  2404  neeq1  2427  neeq2  2428  neleq1  2513  neleq2  2514  dfrex2dc  2535  ralbida  2538  rexbida  2539  ralbidv2  2546  rexbidv2  2547  ralbid2  2548  rexbid2  2549  r19.21t  2619  r19.23t  2652  reubida  2728  rmobida  2734  raleqf  2739  rexeqf  2740  reueq1f  2741  rmoeq1f  2742  cbvraldva2  2787  cbvrexdva2  2788  dfsbcq  3046  sbceqbid  3051  sbcbi2  3095  sbcbid  3102  eqsbc2  3105  sbcabel  3127  sbnfc2  3201  ssconb  3354  uneq1  3368  ineq1  3417  difin2  3485  reuun2  3506  reldisj  3562  undif4  3573  disjssun  3574  sbcssg  3620  eltpg  3736  raltpg  3744  rextpg  3745  r19.12sn  3757  opeq1  3885  opeq2  3886  intmin4  3979  dfiun2g  4025  iindif2m  4061  iinin2m  4062  breq  4113  breq1  4114  breq2  4115  treq  4216  opthg2  4357  poeq1  4422  soeq1  4438  frforeq1  4466  freq1  4467  frforeq2  4468  freq2  4469  frforeq3  4470  weeq1  4479  weeq2  4480  ordeq  4495  limeq  4500  rabxfrd  4592  iunpw  4603  opthprc  4803  releq  4834  sbcrel  4838  eqrel  4841  eqrelrel  4853  xpiindim  4894  brcnvg  4938  brresg  5048  resieq  5050  xpcanm  5204  xpcan2m  5205  dmsnopg  5236  dfco2a  5265  cnvpom  5307  cnvsom  5308  iotaeq  5323  sniota  5345  sbcfung  5378  fneq1  5446  fneq2  5447  feq1  5493  feq2  5494  feq3  5495  sbcfng  5508  sbcfg  5509  f1eq1  5570  f1eq2  5571  f1eq3  5572  foeq1  5588  foeq2  5589  foeq3  5590  f1oeq1  5604  f1oeq2  5605  f1oeq3  5606  fun11iun  5637  mpteqb  5770  dffo3  5826  fmptco  5845  dff13  5943  f1imaeq  5950  f1eqcocnv  5966  fliftcnv  5970  isoeq1  5976  isoeq2  5977  isoeq3  5978  isoeq4  5979  isoeq5  5980  isocnv2  5987  acexmid  6051  fnotovb  6098  mpoeq123  6114  ottposg  6488  dmtpos  6489  smoeq  6523  nnacan  6747  nnmcan  6754  ereq1  6776  ereq2  6777  elecg  6809  ereldm  6814  ixpiinm  6961  enfi  7130  elfi2  7261  fipwssg  7268  ctssdccl  7404  tapeq1  7568  tapeq2  7569  creur  9235  eqreznegel  9949  ltxr  10111  icoshftf1o  10327  elfzm11  10429  elfzomelpfzo  10580  nn0ennn  10799  nnesq  11025  rexfiuz  11678  cau4  11805  sumeq2  12048  fisumcom2  12128  fprodcom2fi  12316  dvdsflip  12541  bitsmod  12646  bitscmp  12648  divgcdcoprm0  12802  hashdvds  12922  4sqlem12  13104  imasaddfnlemg  13544  issgrpv  13634  issgrpn0  13635  mndpropd  13670  ismhm  13691  mhmpropd  13696  issubm2  13703  grppropd  13747  grpinvcnv  13798  conjghm  14010  conjnmzb  14014  ghmpropd  14017  cmnpropd  14029  ablpropd  14030  eqgabl  14064  rngpropd  14116  issrg  14126  ringpropd  14199  crngpropd  14200  opprnzrbg  14347  subrngpropd  14378  resrhm2b  14411  subrgpropd  14415  rhmpropd  14416  opprdomnbg  14437  lmodprop2d  14513  islssm  14522  islssmg  14523  lsspropdg  14596  df2idl2rng  14673  psrbagconf1o  14845  tpspropd  14918  tgss2  14961  lmbr2  15096  txcnmpt  15155  txhmeo  15201  blininf  15306  blres  15316  xmeterval  15317  xmspropd  15359  mspropd  15360  metequiv  15377  xmetxpbl  15390  limcdifap  15544  lgsquadlem1  15967  lgsquadlem2  15968  ushgredgedg  16238  ushgredgedgloop  16240  upgriswlkdc  16372  clwwlknonel  16444  eupth2lem2dc  16471  cbvrald  16577  bj-indeq  16716