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  796  stbid  837  dcbid  843  pm4.14dc  895  orbididc  959  ifpbi123d  998  3orbi123d  1345  3anbi123d  1346  xorbi2d  1422  xorbi1d  1423  nfbidf  1585  drnf1  1779  drnf2  1780  drsb1  1845  sbal2  2071  eubidh  2083  eubid  2084  mobidh  2111  mobid  2112  eqeq1  2236  eqeq2  2239  eleq1w  2290  eleq2w  2291  eleq1  2292  eleq2  2293  cbvabw  2352  eqabdv  2358  nfceqdf  2371  drnfc1  2389  drnfc2  2390  neeq1  2413  neeq2  2414  neleq1  2499  neleq2  2500  dfrex2dc  2521  ralbida  2524  rexbida  2525  ralbidv2  2532  rexbidv2  2533  ralbid2  2534  rexbid2  2535  r19.21t  2605  r19.23t  2638  reubida  2713  rmobida  2719  raleqf  2724  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  cbvraldva2  2772  cbvrexdva2  2773  dfsbcq  3030  sbceqbid  3035  sbcbi2  3079  sbcbid  3086  eqsbc2  3089  sbcabel  3111  sbnfc2  3185  ssconb  3337  uneq1  3351  ineq1  3398  difin2  3466  reuun2  3487  reldisj  3543  undif4  3554  disjssun  3555  sbcssg  3600  eltpg  3711  raltpg  3719  rextpg  3720  r19.12sn  3732  opeq1  3857  opeq2  3858  intmin4  3951  dfiun2g  3997  iindif2m  4033  iinin2m  4034  breq  4085  breq1  4086  breq2  4087  treq  4188  opthg2  4325  poeq1  4390  soeq1  4406  frforeq1  4434  freq1  4435  frforeq2  4436  freq2  4437  frforeq3  4438  weeq1  4447  weeq2  4448  ordeq  4463  limeq  4468  rabxfrd  4560  iunpw  4571  opthprc  4770  releq  4801  sbcrel  4805  eqrel  4808  eqrelrel  4820  xpiindim  4859  brcnvg  4903  brresg  5013  resieq  5015  xpcanm  5168  xpcan2m  5169  dmsnopg  5200  dfco2a  5229  cnvpom  5271  cnvsom  5272  iotaeq  5287  sniota  5309  sbcfung  5342  fneq1  5409  fneq2  5410  feq1  5456  feq2  5457  feq3  5458  sbcfng  5471  sbcfg  5472  f1eq1  5528  f1eq2  5529  f1eq3  5530  foeq1  5546  foeq2  5547  foeq3  5548  f1oeq1  5562  f1oeq2  5563  f1oeq3  5564  fun11iun  5595  mpteqb  5727  dffo3  5784  fmptco  5803  dff13  5898  f1imaeq  5905  f1eqcocnv  5921  fliftcnv  5925  isoeq1  5931  isoeq2  5932  isoeq3  5933  isoeq4  5934  isoeq5  5935  isocnv2  5942  acexmid  6006  fnotovb  6053  mpoeq123  6069  ottposg  6407  dmtpos  6408  smoeq  6442  nnacan  6666  nnmcan  6673  ereq1  6695  ereq2  6696  elecg  6728  ereldm  6733  ixpiinm  6879  enfi  7043  elfi2  7150  fipwssg  7157  ctssdccl  7289  tapeq1  7449  tapeq2  7450  creur  9117  eqreznegel  9821  ltxr  9983  icoshftf1o  10199  elfzm11  10299  elfzomelpfzo  10449  nn0ennn  10667  nnesq  10893  rexfiuz  11515  cau4  11642  sumeq2  11885  fisumcom2  11964  fprodcom2fi  12152  dvdsflip  12377  bitsmod  12482  bitscmp  12484  divgcdcoprm0  12638  hashdvds  12758  4sqlem12  12940  imasaddfnlemg  13362  issgrpv  13452  issgrpn0  13453  mndpropd  13488  ismhm  13509  mhmpropd  13514  issubm2  13521  grppropd  13565  grpinvcnv  13616  conjghm  13828  conjnmzb  13832  ghmpropd  13835  cmnpropd  13847  ablpropd  13848  eqgabl  13882  rngpropd  13933  issrg  13943  ringpropd  14016  crngpropd  14017  opprnzrbg  14164  subrngpropd  14195  resrhm2b  14228  subrgpropd  14232  rhmpropd  14233  opprdomnbg  14253  lmodprop2d  14327  islssm  14336  islssmg  14337  lsspropdg  14410  df2idl2rng  14487  tpspropd  14725  tgss2  14768  lmbr2  14903  txcnmpt  14962  txhmeo  15008  blininf  15113  blres  15123  xmeterval  15124  xmspropd  15166  mspropd  15167  metequiv  15184  xmetxpbl  15197  limcdifap  15351  lgsquadlem1  15771  lgsquadlem2  15772  ushgredgedg  16039  ushgredgedgloop  16041  upgriswlkdc  16101  cbvrald  16207  bj-indeq  16347