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  791  stbid  832  dcbid  838  pm4.14dc  890  orbididc  953  3orbi123d  1311  3anbi123d  1312  xorbi2d  1380  xorbi1d  1381  nfbidf  1537  drnf1  1731  drnf2  1732  drsb1  1797  sbal2  2018  eubidh  2030  eubid  2031  mobidh  2058  mobid  2059  eqeq1  2182  eqeq2  2185  eleq1w  2236  eleq2w  2237  eleq1  2238  eleq2  2239  cbvabw  2298  nfceqdf  2316  drnfc1  2334  drnfc2  2335  neeq1  2358  neeq2  2359  neleq1  2444  neleq2  2445  dfrex2dc  2466  ralbida  2469  rexbida  2470  ralbidv2  2477  rexbidv2  2478  ralbid2  2479  rexbid2  2480  r19.21t  2550  r19.23t  2582  reubida  2656  rmobida  2661  raleqf  2666  rexeqf  2667  reueq1f  2668  rmoeq1f  2669  cbvraldva2  2708  cbvrexdva2  2709  dfsbcq  2962  sbceqbid  2967  sbcbi2  3011  sbcbid  3018  eqsbc2  3021  sbcabel  3042  sbnfc2  3115  ssconb  3266  uneq1  3280  ineq1  3327  difin2  3395  reuun2  3416  reldisj  3472  undif4  3483  disjssun  3484  sbcssg  3530  eltpg  3634  raltpg  3642  rextpg  3643  r19.12sn  3655  opeq1  3774  opeq2  3775  intmin4  3868  dfiun2g  3914  iindif2m  3949  iinin2m  3950  breq  4000  breq1  4001  breq2  4002  treq  4102  opthg2  4233  poeq1  4293  soeq1  4309  frforeq1  4337  freq1  4338  frforeq2  4339  freq2  4340  frforeq3  4341  weeq1  4350  weeq2  4351  ordeq  4366  limeq  4371  rabxfrd  4463  iunpw  4474  opthprc  4671  releq  4702  sbcrel  4706  eqrel  4709  eqrelrel  4721  xpiindim  4757  brcnvg  4801  brresg  4908  resieq  4910  xpcanm  5060  xpcan2m  5061  dmsnopg  5092  dfco2a  5121  cnvpom  5163  cnvsom  5164  iotaeq  5178  sniota  5199  sbcfung  5232  fneq1  5296  fneq2  5297  feq1  5340  feq2  5341  feq3  5342  sbcfng  5355  sbcfg  5356  f1eq1  5408  f1eq2  5409  f1eq3  5410  foeq1  5426  foeq2  5427  foeq3  5428  f1oeq1  5441  f1oeq2  5442  f1oeq3  5443  fun11iun  5474  mpteqb  5598  dffo3  5655  fmptco  5674  dff13  5759  f1imaeq  5766  f1eqcocnv  5782  fliftcnv  5786  isoeq1  5792  isoeq2  5793  isoeq3  5794  isoeq4  5795  isoeq5  5796  isocnv2  5803  acexmid  5864  fnotovb  5908  mpoeq123  5924  ottposg  6246  dmtpos  6247  smoeq  6281  nnacan  6503  nnmcan  6510  ereq1  6532  ereq2  6533  elecg  6563  ereldm  6568  ixpiinm  6714  enfi  6863  elfi2  6961  fipwssg  6968  ctssdccl  7100  creur  8889  eqreznegel  9587  ltxr  9746  icoshftf1o  9962  elfzm11  10061  elfzomelpfzo  10201  nn0ennn  10403  nnesq  10609  rexfiuz  10966  cau4  11093  sumeq2  11335  fisumcom2  11414  fprodcom2fi  11602  dvdsflip  11824  divgcdcoprm0  12068  hashdvds  12188  issgrpv  12676  issgrpn0  12677  mndpropd  12707  ismhm  12716  mhmpropd  12720  grppropd  12755  grpinvcnv  12799  cmnpropd  12897  ablpropd  12898  issrg  12945  ringpropd  13013  crngpropd  13014  tpspropd  13105  tgss2  13150  lmbr2  13285  txcnmpt  13344  txhmeo  13390  blininf  13495  blres  13505  xmeterval  13506  xmspropd  13548  mspropd  13549  metequiv  13566  xmetxpbl  13579  limcdifap  13702  cbvrald  14100  bj-indeq  14241