Theorem 3bitr4g 222

Description: More general version of 3bitr4i 211. 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	syl5bb 191	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 197	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1d  232  pm5.32rd  447  orbi1d  781  stbid  818  dcbid  824  pm4.14dc  876  orbididc  938  3orbi123d  1293  3anbi123d  1294  xorbi2d  1362  xorbi1d  1363  nfbidf  1519  drnf1  1713  drnf2  1714  drsb1  1779  sbal2  2000  eubidh  2012  eubid  2013  mobidh  2040  mobid  2041  eqeq1  2164  eqeq2  2167  eleq1w  2218  eleq2w  2219  eleq1  2220  eleq2  2221  cbvabw  2280  nfceqdf  2298  drnfc1  2316  drnfc2  2317  neeq1  2340  neeq2  2341  neleq1  2426  neleq2  2427  dfrex2dc  2448  ralbida  2451  rexbida  2452  ralbidv2  2459  rexbidv2  2460  ralbid2  2461  rexbid2  2462  r19.21t  2532  r19.23t  2564  reubida  2638  rmobida  2643  raleqf  2648  rexeqf  2649  reueq1f  2650  rmoeq1f  2651  cbvraldva2  2687  cbvrexdva2  2688  dfsbcq  2939  sbcbi2  2987  sbcbid  2994  eqsbc3r  2997  sbcabel  3018  sbnfc2  3091  ssconb  3240  uneq1  3254  ineq1  3301  difin2  3369  reuun2  3390  reldisj  3445  undif4  3456  disjssun  3457  sbcssg  3503  eltpg  3604  raltpg  3612  rextpg  3613  r19.12sn  3625  opeq1  3741  opeq2  3742  intmin4  3835  dfiun2g  3881  iindif2m  3916  iinin2m  3917  breq  3967  breq1  3968  breq2  3969  treq  4068  opthg2  4198  poeq1  4258  soeq1  4274  frforeq1  4302  freq1  4303  frforeq2  4304  freq2  4305  frforeq3  4306  weeq1  4315  weeq2  4316  ordeq  4331  limeq  4336  rabxfrd  4427  iunpw  4438  opthprc  4634  releq  4665  sbcrel  4669  eqrel  4672  eqrelrel  4684  xpiindim  4720  brcnvg  4764  brresg  4871  resieq  4873  xpcanm  5022  xpcan2m  5023  dmsnopg  5054  dfco2a  5083  cnvpom  5125  cnvsom  5126  iotaeq  5140  sniota  5159  sbcfung  5191  fneq1  5255  fneq2  5256  feq1  5299  feq2  5300  feq3  5301  sbcfng  5314  sbcfg  5315  f1eq1  5367  f1eq2  5368  f1eq3  5369  foeq1  5385  foeq2  5386  foeq3  5387  f1oeq1  5400  f1oeq2  5401  f1oeq3  5402  fun11iun  5432  mpteqb  5555  dffo3  5611  fmptco  5630  dff13  5713  f1imaeq  5720  f1eqcocnv  5736  fliftcnv  5740  isoeq1  5746  isoeq2  5747  isoeq3  5748  isoeq4  5749  isoeq5  5750  isocnv2  5757  acexmid  5817  fnotovb  5858  mpoeq123  5874  ottposg  6196  dmtpos  6197  smoeq  6231  nnacan  6452  nnmcan  6459  ereq1  6480  ereq2  6481  elecg  6511  ereldm  6516  ixpiinm  6662  enfi  6811  elfi2  6909  fipwssg  6916  ctssdccl  7045  creur  8813  eqreznegel  9505  ltxr  9664  icoshftf1o  9877  elfzm11  9975  elfzomelpfzo  10112  nn0ennn  10314  nnesq  10519  rexfiuz  10871  cau4  10998  sumeq2  11238  fisumcom2  11317  fprodcom2fi  11505  dvdsflip  11724  divgcdcoprm0  11958  hashdvds  12073  tpspropd  12394  tgss2  12439  lmbr2  12574  txcnmpt  12633  txhmeo  12679  blininf  12784  blres  12794  xmeterval  12795  xmspropd  12837  mspropd  12838  metequiv  12855  xmetxpbl  12868  limcdifap  12991  cbvrald  13322