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  448  orbi1d  786  stbid  827  dcbid  833  pm4.14dc  885  orbididc  948  3orbi123d  1306  3anbi123d  1307  xorbi2d  1375  xorbi1d  1376  nfbidf  1532  drnf1  1726  drnf2  1727  drsb1  1792  sbal2  2013  eubidh  2025  eubid  2026  mobidh  2053  mobid  2054  eqeq1  2177  eqeq2  2180  eleq1w  2231  eleq2w  2232  eleq1  2233  eleq2  2234  cbvabw  2293  nfceqdf  2311  drnfc1  2329  drnfc2  2330  neeq1  2353  neeq2  2354  neleq1  2439  neleq2  2440  dfrex2dc  2461  ralbida  2464  rexbida  2465  ralbidv2  2472  rexbidv2  2473  ralbid2  2474  rexbid2  2475  r19.21t  2545  r19.23t  2577  reubida  2651  rmobida  2656  raleqf  2661  rexeqf  2662  reueq1f  2663  rmoeq1f  2664  cbvraldva2  2703  cbvrexdva2  2704  dfsbcq  2957  sbcbi2  3005  sbcbid  3012  eqsbc2  3015  sbcabel  3036  sbnfc2  3109  ssconb  3260  uneq1  3274  ineq1  3321  difin2  3389  reuun2  3410  reldisj  3466  undif4  3477  disjssun  3478  sbcssg  3524  eltpg  3628  raltpg  3636  rextpg  3637  r19.12sn  3649  opeq1  3765  opeq2  3766  intmin4  3859  dfiun2g  3905  iindif2m  3940  iinin2m  3941  breq  3991  breq1  3992  breq2  3993  treq  4093  opthg2  4224  poeq1  4284  soeq1  4300  frforeq1  4328  freq1  4329  frforeq2  4330  freq2  4331  frforeq3  4332  weeq1  4341  weeq2  4342  ordeq  4357  limeq  4362  rabxfrd  4454  iunpw  4465  opthprc  4662  releq  4693  sbcrel  4697  eqrel  4700  eqrelrel  4712  xpiindim  4748  brcnvg  4792  brresg  4899  resieq  4901  xpcanm  5050  xpcan2m  5051  dmsnopg  5082  dfco2a  5111  cnvpom  5153  cnvsom  5154  iotaeq  5168  sniota  5189  sbcfung  5222  fneq1  5286  fneq2  5287  feq1  5330  feq2  5331  feq3  5332  sbcfng  5345  sbcfg  5346  f1eq1  5398  f1eq2  5399  f1eq3  5400  foeq1  5416  foeq2  5417  foeq3  5418  f1oeq1  5431  f1oeq2  5432  f1oeq3  5433  fun11iun  5463  mpteqb  5586  dffo3  5643  fmptco  5662  dff13  5747  f1imaeq  5754  f1eqcocnv  5770  fliftcnv  5774  isoeq1  5780  isoeq2  5781  isoeq3  5782  isoeq4  5783  isoeq5  5784  isocnv2  5791  acexmid  5852  fnotovb  5896  mpoeq123  5912  ottposg  6234  dmtpos  6235  smoeq  6269  nnacan  6491  nnmcan  6498  ereq1  6520  ereq2  6521  elecg  6551  ereldm  6556  ixpiinm  6702  enfi  6851  elfi2  6949  fipwssg  6956  ctssdccl  7088  creur  8875  eqreznegel  9573  ltxr  9732  icoshftf1o  9948  elfzm11  10047  elfzomelpfzo  10187  nn0ennn  10389  nnesq  10595  rexfiuz  10953  cau4  11080  sumeq2  11322  fisumcom2  11401  fprodcom2fi  11589  dvdsflip  11811  divgcdcoprm0  12055  hashdvds  12175  issgrpv  12645  issgrpn0  12646  mndpropd  12676  ismhm  12685  mhmpropd  12689  grppropd  12724  grpinvcnv  12767  tpspropd  12828  tgss2  12873  lmbr2  13008  txcnmpt  13067  txhmeo  13113  blininf  13218  blres  13228  xmeterval  13229  xmspropd  13271  mspropd  13272  metequiv  13289  xmetxpbl  13302  limcdifap  13425  cbvrald  13823  bj-indeq  13964