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  9289  eqreznegel  10014  ltxr  10177  icoshftf1o  10393  elfzm11  10498  elfzomelpfzo  10649  nn0ennn  10870  nnesq  11097  hashf1lem1  11285  rexfiuz  11755  cau4  11882  sumeq2  12125  fisumcom2  12205  fprodcom2fi  12393  dvdsflip  12618  bitsmod  12723  bitscmp  12725  divgcdcoprm0  12879  hashdvds  12999  4sqlem12  13181  imasaddfnlemg  13635  issgrpv  13719  issgrpn0  13720  mndpropd  13753  ismhm  13768  mhmpropd  13773  issubm2  13780  grppropd  13822  grpinvcnv  13873  conjghm  14079  conjnmzb  14083  ghmpropd  14086  cmnpropd  14098  ablpropd  14099  eqgabl  14134  rngpropd  14254  issrg  14269  ringpropd  14343  crngpropd  14344  opprnzrbg  14492  opprlring  14504  subrngpropd  14524  resrhm2b  14557  subrgpropd  14561  rhmpropd  14562  opprdomnbg  14583  opprdrng  14620  lmodprop2d  14685  islssm  14694  islssmg  14695  lsspropdg  14768  df2idl2rng  14845  assapropd  15014  psrbagconf1o  15064  tpspropd  15137  tgss2  15180  lmbr2  15315  txcnmpt  15374  txhmeo  15420  blininf  15525  blres  15535  xmeterval  15536  xmspropd  15578  mspropd  15579  metequiv  15596  xmetxpbl  15609  limcdifap  15763  lgsquadlem1  16196  lgsquadlem2  16197  ushgredgedg  16467  ushgredgedgloop  16469  upgriswlkdc  16601  clwwlknonel  16673  eupth2lem2dc  16700  cbvrald  16816  bj-indeq  16955  alsbid  17143