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  799  stbid  840  dcbid  846  pm4.14dc  898  orbididc  962  ifpbi123d  1001  3orbi123d  1348  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  nfbidf  1588  drnf1  1781  drnf2  1782  drsb1  1847  sbal2  2073  eubidh  2085  eubid  2086  mobidh  2113  mobid  2114  eqeq1  2238  eqeq2  2241  eleq1w  2292  eleq2w  2293  eleq1  2294  eleq2  2295  cbvabw  2355  eqabdv  2361  nfceqdf  2374  drnfc1  2392  drnfc2  2393  neeq1  2416  neeq2  2417  neleq1  2502  neleq2  2503  dfrex2dc  2524  ralbida  2527  rexbida  2528  ralbidv2  2535  rexbidv2  2536  ralbid2  2537  rexbid2  2538  r19.21t  2608  r19.23t  2641  reubida  2716  rmobida  2722  raleqf  2727  rexeqf  2728  reueq1f  2729  rmoeq1f  2730  cbvraldva2  2775  cbvrexdva2  2776  dfsbcq  3034  sbceqbid  3039  sbcbi2  3083  sbcbid  3090  eqsbc2  3093  sbcabel  3115  sbnfc2  3189  ssconb  3342  uneq1  3356  ineq1  3403  difin2  3471  reuun2  3492  reldisj  3548  undif4  3559  disjssun  3560  sbcssg  3605  eltpg  3718  raltpg  3726  rextpg  3727  r19.12sn  3739  opeq1  3867  opeq2  3868  intmin4  3961  dfiun2g  4007  iindif2m  4043  iinin2m  4044  breq  4095  breq1  4096  breq2  4097  treq  4198  opthg2  4337  poeq1  4402  soeq1  4418  frforeq1  4446  freq1  4447  frforeq2  4448  freq2  4449  frforeq3  4450  weeq1  4459  weeq2  4460  ordeq  4475  limeq  4480  rabxfrd  4572  iunpw  4583  opthprc  4783  releq  4814  sbcrel  4818  eqrel  4821  eqrelrel  4833  xpiindim  4873  brcnvg  4917  brresg  5027  resieq  5029  xpcanm  5183  xpcan2m  5184  dmsnopg  5215  dfco2a  5244  cnvpom  5286  cnvsom  5287  iotaeq  5302  sniota  5324  sbcfung  5357  fneq1  5425  fneq2  5426  feq1  5472  feq2  5473  feq3  5474  sbcfng  5487  sbcfg  5488  f1eq1  5546  f1eq2  5547  f1eq3  5548  foeq1  5564  foeq2  5565  foeq3  5566  f1oeq1  5580  f1oeq2  5581  f1oeq3  5582  fun11iun  5613  mpteqb  5746  dffo3  5802  fmptco  5821  dff13  5919  f1imaeq  5926  f1eqcocnv  5942  fliftcnv  5946  isoeq1  5952  isoeq2  5953  isoeq3  5954  isoeq4  5955  isoeq5  5956  isocnv2  5963  acexmid  6027  fnotovb  6074  mpoeq123  6090  ottposg  6464  dmtpos  6465  smoeq  6499  nnacan  6723  nnmcan  6730  ereq1  6752  ereq2  6753  elecg  6785  ereldm  6790  ixpiinm  6936  enfi  7103  elfi2  7214  fipwssg  7221  ctssdccl  7353  tapeq1  7514  tapeq2  7515  creur  9181  eqreznegel  9892  ltxr  10054  icoshftf1o  10270  elfzm11  10371  elfzomelpfzo  10522  nn0ennn  10741  nnesq  10967  rexfiuz  11612  cau4  11739  sumeq2  11982  fisumcom2  12062  fprodcom2fi  12250  dvdsflip  12475  bitsmod  12580  bitscmp  12582  divgcdcoprm0  12736  hashdvds  12856  4sqlem12  13038  imasaddfnlemg  13460  issgrpv  13550  issgrpn0  13551  mndpropd  13586  ismhm  13607  mhmpropd  13612  issubm2  13619  grppropd  13663  grpinvcnv  13714  conjghm  13926  conjnmzb  13930  ghmpropd  13933  cmnpropd  13945  ablpropd  13946  eqgabl  13980  rngpropd  14032  issrg  14042  ringpropd  14115  crngpropd  14116  opprnzrbg  14263  subrngpropd  14294  resrhm2b  14327  subrgpropd  14331  rhmpropd  14332  opprdomnbg  14353  lmodprop2d  14427  islssm  14436  islssmg  14437  lsspropdg  14510  df2idl2rng  14587  psrbagconf1o  14757  tpspropd  14830  tgss2  14873  lmbr2  15008  txcnmpt  15067  txhmeo  15113  blininf  15218  blres  15228  xmeterval  15229  xmspropd  15271  mspropd  15272  metequiv  15289  xmetxpbl  15302  limcdifap  15456  lgsquadlem1  15879  lgsquadlem2  15880  ushgredgedg  16150  ushgredgedgloop  16152  upgriswlkdc  16284  clwwlknonel  16356  eupth2lem2dc  16383  cbvrald  16489  bj-indeq  16628