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	syl6bbr 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  1290  3anbi123d  1291  xorbi2d  1359  xorbi1d  1360  nfbidf  1520  drnf1  1712  drnf2  1713  drsb1  1772  sbal2  1998  eubidh  2006  eubid  2007  mobidh  2034  mobid  2035  eqeq1  2147  eqeq2  2150  eleq1w  2201  eleq2w  2202  eleq1  2203  eleq2  2204  nfceqdf  2281  drnfc1  2299  drnfc2  2300  neeq1  2322  neeq2  2323  neleq1  2408  neleq2  2409  dfrex2dc  2429  ralbida  2432  rexbida  2433  ralbidv2  2440  rexbidv2  2441  ralbid2  2442  rexbid2  2443  r19.21t  2510  r19.23t  2542  reubida  2615  rmobida  2620  raleqf  2625  rexeqf  2626  reueq1f  2627  rmoeq1f  2628  cbvraldva2  2664  cbvrexdva2  2665  dfsbcq  2915  sbcbi2  2963  sbcbid  2970  eqsbc3r  2973  sbcabel  2994  sbnfc2  3065  ssconb  3214  uneq1  3228  ineq1  3275  difin2  3343  reuun2  3364  reldisj  3419  undif4  3430  disjssun  3431  sbcssg  3477  eltpg  3576  raltpg  3584  rextpg  3585  r19.12sn  3597  opeq1  3713  opeq2  3714  intmin4  3807  dfiun2g  3853  iindif2m  3888  iinin2m  3889  breq  3939  breq1  3940  breq2  3941  treq  4040  opthg2  4169  poeq1  4229  soeq1  4245  frforeq1  4273  freq1  4274  frforeq2  4275  freq2  4276  frforeq3  4277  weeq1  4286  weeq2  4287  ordeq  4302  limeq  4307  rabxfrd  4398  iunpw  4409  opthprc  4598  releq  4629  sbcrel  4633  eqrel  4636  eqrelrel  4648  xpiindim  4684  brcnvg  4728  brresg  4835  resieq  4837  xpcanm  4986  xpcan2m  4987  dmsnopg  5018  dfco2a  5047  cnvpom  5089  cnvsom  5090  iotaeq  5104  sniota  5123  sbcfung  5155  fneq1  5219  fneq2  5220  feq1  5263  feq2  5264  feq3  5265  sbcfng  5278  sbcfg  5279  f1eq1  5331  f1eq2  5332  f1eq3  5333  foeq1  5349  foeq2  5350  foeq3  5351  f1oeq1  5364  f1oeq2  5365  f1oeq3  5366  fun11iun  5396  mpteqb  5519  dffo3  5575  fmptco  5594  dff13  5677  f1imaeq  5684  f1eqcocnv  5700  fliftcnv  5704  isoeq1  5710  isoeq2  5711  isoeq3  5712  isoeq4  5713  isoeq5  5714  isocnv2  5721  acexmid  5781  fnotovb  5822  mpoeq123  5838  ottposg  6160  dmtpos  6161  smoeq  6195  nnacan  6416  nnmcan  6423  ereq1  6444  ereq2  6445  elecg  6475  ereldm  6480  ixpiinm  6626  enfi  6775  elfi2  6868  fipwssg  6875  ctssdccl  7004  creur  8741  eqreznegel  9433  ltxr  9592  icoshftf1o  9804  elfzm11  9902  elfzomelpfzo  10039  nn0ennn  10237  nnesq  10442  rexfiuz  10793  cau4  10920  sumeq2  11160  fisumcom2  11239  dvdsflip  11585  divgcdcoprm0  11818  hashdvds  11933  tpspropd  12242  tgss2  12287  lmbr2  12422  txcnmpt  12481  txhmeo  12527  blininf  12632  blres  12642  xmeterval  12643  xmspropd  12685  mspropd  12686  metequiv  12703  xmetxpbl  12716  limcdifap  12839  cbvrald  13166