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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bibi1d  233  pm5.32rd  455  orbi1d  803  stbid  844  dcbid  850  pm4.14dc  902  orbididc  966  ifpbi123d  1005  3orbi123d  1352  3anbi123d  1353  xorbi2d  1429  xorbi1d  1430  nfbidf  1592  drnf1  1786  drnf2  1787  drsb1  1852  sbal2  2080  eubidh  2092  eubid  2093  mobidh  2120  mobid  2121  eqeq1  2245  eqeq2  2248  eleq1w  2299  eleq2w  2300  eleq1  2301  eleq2  2302  abbi  2357  cbvabw  2363  eqabdv  2369  nfceqdf  2391  drnfc1  2409  drnfc2  2410  neeq1  2433  neeq2  2434  neleq1  2519  neleq2  2520  dfrex2dc  2541  ralbida  2544  rexbida  2545  ralbidv2  2552  rexbidv2  2553  ralbid2  2554  rexbid2  2555  r19.21t  2625  r19.23t  2658  reubida  2734  rmobida  2740  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  cbvraldva2  2793  cbvrexdva2  2794  dfsbcq  3053  sbceqbid  3058  sbcbi2  3102  sbcbid  3109  eqsbc2  3112  sbcabel  3134  sbnfc2  3208  ssconb  3362  uneq1  3376  ineq1  3425  difin2  3493  reuun2  3516  reldisj  3576  undif4  3587  disjssun  3588  sbcssg  3636  eltpg  3754  raltpg  3762  rextpg  3763  r19.12sn  3775  opeq1  3904  opeq2  3905  intmin4  3998  dfiun2g  4044  iindif2m  4080  iinin2m  4081  breq  4132  breq1  4133  breq2  4134  treq  4235  opthg2  4379  poeq1  4444  soeq1  4460  frforeq1  4488  freq1  4489  frforeq2  4490  freq2  4491  frforeq3  4492  weeq1  4501  weeq2  4502  ordeq  4517  limeq  4522  rabxfrd  4615  iunpw  4626  opthprc  4826  releq  4857  sbcrel  4861  eqrel  4864  eqrelrel  4876  xpiindim  4917  brcnvg  4961  brresg  5071  resieq  5073  xpcanm  5227  xpcan2m  5228  dmsnopg  5259  dfco2a  5288  cnvpom  5330  cnvsom  5331  iotaeq  5346  sniota  5368  sbcfung  5401  fneq1  5469  fneq2  5470  feq1  5516  feq2  5517  feq3  5518  sbcfng  5531  sbcfg  5532  f1eq1  5593  f1eq2  5594  f1eq3  5595  foeq1  5611  foeq2  5612  foeq3  5613  f1oeq1  5627  f1oeq2  5628  f1oeq3  5629  fun11iun  5660  mpteqb  5796  dffo3  5855  fmptco  5874  dff13  5974  f1imaeq  5981  f1eqcocnv  5997  fliftcnv  6001  isoeq1  6007  isoeq2  6008  isoeq3  6009  isoeq4  6010  isoeq5  6011  isocnv2  6018  acexmid  6084  fnotovb  6131  mpoeq123  6147  ottposg  6526  dmtpos  6527  smoeq  6561  nnacan  6785  nnmcan  6792  ereq1  6814  ereq2  6815  elecg  6847  ereldm  6852  ixpiinm  7006  enfi  7175  elfi2  7306  fipwssg  7313  ctssdccl  7451  papeq1  7609  papeq2  7610  tapeq1  7618  tapeq2  7619  creur  9291  eqreznegel  10023  ltxr  10187  icoshftf1o  10403  elfzm11  10508  elfzomelpfzo  10659  nn0ennn  10883  nnesq  11110  hashf1lem1  11299  rexfiuz  11769  cau4  11897  sumeq2  12141  fisumcom2  12221  fprodcom2fi  12409  dvdsflip  12634  bitsmod  12739  bitscmp  12741  divgcdcoprm0  12895  hashdvds  13019  4sqlem12  13201  imasaddfnlemg  13684  issgrpv  13768  issgrpn0  13769  mndpropd  13802  ismhm  13817  mhmpropd  13822  issubm2  13829  grppropd  13871  grpinvcnv  13922  conjghm  14128  conjnmzb  14132  ghmpropd  14135  cmnpropd  14147  ablpropd  14148  eqgabl  14183  rngpropd  14303  issrg  14318  ringpropd  14392  crngpropd  14393  opprnzrbg  14541  opprlring  14553  subrngpropd  14573  resrhm2b  14606  subrgpropd  14610  rhmpropd  14611  opprdomnbg  14632  opprdrng  14669  lmodprop2d  14734  islssm  14743  islssmg  14744  lsspropdg  14817  df2idl2rng  14894  assapropd  15063  psrbagconf1o  15113  tpspropd  15186  tgss2  15229  lmbr2  15364  txcnmpt  15423  txhmeo  15469  blininf  15574  blres  15584  xmeterval  15585  xmspropd  15627  mspropd  15628  metequiv  15645  xmetxpbl  15658  limcdifap  15812  lgsquadlem1  16294  lgsquadlem2  16295  ushgredgedg  16565  ushgredgedgloop  16567  upgriswlkdc  16699  clwwlknonel  16771  eupth2lem2dc  16798  cbvrald  16914  bj-indeq  17053  alsbid  17241