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  822  dcbid  828  pm4.14dc  880  orbididc  943  3orbi123d  1301  3anbi123d  1302  xorbi2d  1370  xorbi1d  1371  nfbidf  1527  drnf1  1721  drnf2  1722  drsb1  1787  sbal2  2008  eubidh  2020  eubid  2021  mobidh  2048  mobid  2049  eqeq1  2172  eqeq2  2175  eleq1w  2227  eleq2w  2228  eleq1  2229  eleq2  2230  cbvabw  2289  nfceqdf  2307  drnfc1  2325  drnfc2  2326  neeq1  2349  neeq2  2350  neleq1  2435  neleq2  2436  dfrex2dc  2457  ralbida  2460  rexbida  2461  ralbidv2  2468  rexbidv2  2469  ralbid2  2470  rexbid2  2471  r19.21t  2541  r19.23t  2573  reubida  2647  rmobida  2652  raleqf  2657  rexeqf  2658  reueq1f  2659  rmoeq1f  2660  cbvraldva2  2699  cbvrexdva2  2700  dfsbcq  2953  sbcbi2  3001  sbcbid  3008  eqsbc2  3011  sbcabel  3032  sbnfc2  3105  ssconb  3255  uneq1  3269  ineq1  3316  difin2  3384  reuun2  3405  reldisj  3460  undif4  3471  disjssun  3472  sbcssg  3518  eltpg  3621  raltpg  3629  rextpg  3630  r19.12sn  3642  opeq1  3758  opeq2  3759  intmin4  3852  dfiun2g  3898  iindif2m  3933  iinin2m  3934  breq  3984  breq1  3985  breq2  3986  treq  4086  opthg2  4217  poeq1  4277  soeq1  4293  frforeq1  4321  freq1  4322  frforeq2  4323  freq2  4324  frforeq3  4325  weeq1  4334  weeq2  4335  ordeq  4350  limeq  4355  rabxfrd  4447  iunpw  4458  opthprc  4655  releq  4686  sbcrel  4690  eqrel  4693  eqrelrel  4705  xpiindim  4741  brcnvg  4785  brresg  4892  resieq  4894  xpcanm  5043  xpcan2m  5044  dmsnopg  5075  dfco2a  5104  cnvpom  5146  cnvsom  5147  iotaeq  5161  sniota  5180  sbcfung  5212  fneq1  5276  fneq2  5277  feq1  5320  feq2  5321  feq3  5322  sbcfng  5335  sbcfg  5336  f1eq1  5388  f1eq2  5389  f1eq3  5390  foeq1  5406  foeq2  5407  foeq3  5408  f1oeq1  5421  f1oeq2  5422  f1oeq3  5423  fun11iun  5453  mpteqb  5576  dffo3  5632  fmptco  5651  dff13  5736  f1imaeq  5743  f1eqcocnv  5759  fliftcnv  5763  isoeq1  5769  isoeq2  5770  isoeq3  5771  isoeq4  5772  isoeq5  5773  isocnv2  5780  acexmid  5841  fnotovb  5885  mpoeq123  5901  ottposg  6223  dmtpos  6224  smoeq  6258  nnacan  6480  nnmcan  6487  ereq1  6508  ereq2  6509  elecg  6539  ereldm  6544  ixpiinm  6690  enfi  6839  elfi2  6937  fipwssg  6944  ctssdccl  7076  creur  8854  eqreznegel  9552  ltxr  9711  icoshftf1o  9927  elfzm11  10026  elfzomelpfzo  10166  nn0ennn  10368  nnesq  10574  rexfiuz  10931  cau4  11058  sumeq2  11300  fisumcom2  11379  fprodcom2fi  11567  dvdsflip  11789  divgcdcoprm0  12033  hashdvds  12153  issgrpv  12622  issgrpn0  12623  tpspropd  12684  tgss2  12729  lmbr2  12864  txcnmpt  12923  txhmeo  12969  blininf  13074  blres  13084  xmeterval  13085  xmspropd  13127  mspropd  13128  metequiv  13145  xmetxpbl  13158  limcdifap  13281  cbvrald  13679  bj-indeq  13821