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	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4g.2	⊢ (𝜃 ↔ 𝜓)
3bitr4g.3	⊢ (𝜏 ↔ 𝜒)

Assertion

Ref	Expression
3bitr4g	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.2	. . 3 ⊢ (𝜃 ↔ 𝜓)
2		3bitr4g.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitrid 192	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 198	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

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  3047  sbceqbid  3052  sbcbi2  3096  sbcbid  3103  eqsbc2  3106  sbcabel  3128  sbnfc2  3202  ssconb  3356  uneq1  3370  ineq1  3419  difin2  3487  reuun2  3508  reldisj  3564  undif4  3575  disjssun  3576  sbcssg  3622  eltpg  3739  raltpg  3747  rextpg  3748  r19.12sn  3760  opeq1  3888  opeq2  3889  intmin4  3982  dfiun2g  4028  iindif2m  4064  iinin2m  4065  breq  4116  breq1  4117  breq2  4118  treq  4219  opthg2  4360  poeq1  4425  soeq1  4441  frforeq1  4469  freq1  4470  frforeq2  4471  freq2  4472  frforeq3  4473  weeq1  4482  weeq2  4483  ordeq  4498  limeq  4503  rabxfrd  4595  iunpw  4606  opthprc  4806  releq  4837  sbcrel  4841  eqrel  4844  eqrelrel  4856  xpiindim  4897  brcnvg  4941  brresg  5051  resieq  5053  xpcanm  5207  xpcan2m  5208  dmsnopg  5239  dfco2a  5268  cnvpom  5310  cnvsom  5311  iotaeq  5326  sniota  5348  sbcfung  5381  fneq1  5449  fneq2  5450  feq1  5496  feq2  5497  feq3  5498  sbcfng  5511  sbcfg  5512  f1eq1  5573  f1eq2  5574  f1eq3  5575  foeq1  5591  foeq2  5592  foeq3  5593  f1oeq1  5607  f1oeq2  5608  f1oeq3  5609  fun11iun  5640  mpteqb  5773  dffo3  5829  fmptco  5848  dff13  5947  f1imaeq  5954  f1eqcocnv  5970  fliftcnv  5974  isoeq1  5980  isoeq2  5981  isoeq3  5982  isoeq4  5983  isoeq5  5984  isocnv2  5991  acexmid  6057  fnotovb  6104  mpoeq123  6120  ottposg  6499  dmtpos  6500  smoeq  6534  nnacan  6758  nnmcan  6765  ereq1  6787  ereq2  6788  elecg  6820  ereldm  6825  ixpiinm  6972  enfi  7141  elfi2  7272  fipwssg  7279  ctssdccl  7415  papeq1  7573  papeq2  7574  tapeq1  7582  tapeq2  7583  creur  9250  eqreznegel  9964  ltxr  10127  icoshftf1o  10343  elfzm11  10447  elfzomelpfzo  10598  nn0ennn  10819  nnesq  11046  rexfiuz  11699  cau4  11826  sumeq2  12069  fisumcom2  12149  fprodcom2fi  12337  dvdsflip  12562  bitsmod  12667  bitscmp  12669  divgcdcoprm0  12823  hashdvds  12943  4sqlem12  13125  imasaddfnlemg  13578  issgrpv  13667  issgrpn0  13668  mndpropd  13701  ismhm  13716  mhmpropd  13721  issubm2  13728  grppropd  13772  grpinvcnv  13823  conjghm  14029  conjnmzb  14033  ghmpropd  14036  cmnpropd  14048  ablpropd  14049  eqgabl  14083  rngpropd  14194  issrg  14208  ringpropd  14281  crngpropd  14282  opprnzrbg  14430  opprlring  14442  subrngpropd  14462  resrhm2b  14495  subrgpropd  14499  rhmpropd  14500  opprdomnbg  14521  opprdrng  14558  lmodprop2d  14622  islssm  14631  islssmg  14632  lsspropdg  14705  df2idl2rng  14782  psrbagconf1o  14954  tpspropd  15027  tgss2  15070  lmbr2  15205  txcnmpt  15264  txhmeo  15310  blininf  15415  blres  15425  xmeterval  15426  xmspropd  15468  mspropd  15469  metequiv  15486  xmetxpbl  15499  limcdifap  15653  lgsquadlem1  16076  lgsquadlem2  16077  ushgredgedg  16347  ushgredgedgloop  16349  upgriswlkdc  16481  clwwlknonel  16553  eupth2lem2dc  16580  cbvrald  16686  bj-indeq  16825