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  3031  sbceqbid  3036  sbcbi2  3080  sbcbid  3087  eqsbc2  3090  sbcabel  3112  sbnfc2  3186  ssconb  3338  uneq1  3352  ineq1  3399  difin2  3467  reuun2  3488  reldisj  3544  undif4  3555  disjssun  3556  sbcssg  3601  eltpg  3712  raltpg  3720  rextpg  3721  r19.12sn  3733  opeq1  3860  opeq2  3861  intmin4  3954  dfiun2g  4000  iindif2m  4036  iinin2m  4037  breq  4088  breq1  4089  breq2  4090  treq  4191  opthg2  4329  poeq1  4394  soeq1  4410  frforeq1  4438  freq1  4439  frforeq2  4440  freq2  4441  frforeq3  4442  weeq1  4451  weeq2  4452  ordeq  4467  limeq  4472  rabxfrd  4564  iunpw  4575  opthprc  4775  releq  4806  sbcrel  4810  eqrel  4813  eqrelrel  4825  xpiindim  4865  brcnvg  4909  brresg  5019  resieq  5021  xpcanm  5174  xpcan2m  5175  dmsnopg  5206  dfco2a  5235  cnvpom  5277  cnvsom  5278  iotaeq  5293  sniota  5315  sbcfung  5348  fneq1  5415  fneq2  5416  feq1  5462  feq2  5463  feq3  5464  sbcfng  5477  sbcfg  5478  f1eq1  5534  f1eq2  5535  f1eq3  5536  foeq1  5552  foeq2  5553  foeq3  5554  f1oeq1  5568  f1oeq2  5569  f1oeq3  5570  fun11iun  5601  mpteqb  5733  dffo3  5790  fmptco  5809  dff13  5904  f1imaeq  5911  f1eqcocnv  5927  fliftcnv  5931  isoeq1  5937  isoeq2  5938  isoeq3  5939  isoeq4  5940  isoeq5  5941  isocnv2  5948  acexmid  6012  fnotovb  6059  mpoeq123  6075  ottposg  6416  dmtpos  6417  smoeq  6451  nnacan  6675  nnmcan  6682  ereq1  6704  ereq2  6705  elecg  6737  ereldm  6742  ixpiinm  6888  enfi  7055  elfi2  7162  fipwssg  7169  ctssdccl  7301  tapeq1  7461  tapeq2  7462  creur  9129  eqreznegel  9838  ltxr  10000  icoshftf1o  10216  elfzm11  10316  elfzomelpfzo  10466  nn0ennn  10685  nnesq  10911  rexfiuz  11540  cau4  11667  sumeq2  11910  fisumcom2  11989  fprodcom2fi  12177  dvdsflip  12402  bitsmod  12507  bitscmp  12509  divgcdcoprm0  12663  hashdvds  12783  4sqlem12  12965  imasaddfnlemg  13387  issgrpv  13477  issgrpn0  13478  mndpropd  13513  ismhm  13534  mhmpropd  13539  issubm2  13546  grppropd  13590  grpinvcnv  13641  conjghm  13853  conjnmzb  13857  ghmpropd  13860  cmnpropd  13872  ablpropd  13873  eqgabl  13907  rngpropd  13958  issrg  13968  ringpropd  14041  crngpropd  14042  opprnzrbg  14189  subrngpropd  14220  resrhm2b  14253  subrgpropd  14257  rhmpropd  14258  opprdomnbg  14278  lmodprop2d  14352  islssm  14361  islssmg  14362  lsspropdg  14435  df2idl2rng  14512  tpspropd  14750  tgss2  14793  lmbr2  14928  txcnmpt  14987  txhmeo  15033  blininf  15138  blres  15148  xmeterval  15149  xmspropd  15191  mspropd  15192  metequiv  15209  xmetxpbl  15222  limcdifap  15376  lgsquadlem1  15796  lgsquadlem2  15797  ushgredgedg  16065  ushgredgedgloop  16067  upgriswlkdc  16157  clwwlknonel  16227  cbvrald  16320  bj-indeq  16460