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  792  stbid  833  dcbid  839  pm4.14dc  891  orbididc  955  3orbi123d  1322  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  nfbidf  1553  drnf1  1747  drnf2  1748  drsb1  1813  sbal2  2039  eubidh  2051  eubid  2052  mobidh  2079  mobid  2080  eqeq1  2203  eqeq2  2206  eleq1w  2257  eleq2w  2258  eleq1  2259  eleq2  2260  cbvabw  2319  eqabdv  2325  nfceqdf  2338  drnfc1  2356  drnfc2  2357  neeq1  2380  neeq2  2381  neleq1  2466  neleq2  2467  dfrex2dc  2488  ralbida  2491  rexbida  2492  ralbidv2  2499  rexbidv2  2500  ralbid2  2501  rexbid2  2502  r19.21t  2572  r19.23t  2604  reubida  2679  rmobida  2684  raleqf  2689  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  cbvraldva2  2736  cbvrexdva2  2737  dfsbcq  2991  sbceqbid  2996  sbcbi2  3040  sbcbid  3047  eqsbc2  3050  sbcabel  3071  sbnfc2  3145  ssconb  3297  uneq1  3311  ineq1  3358  difin2  3426  reuun2  3447  reldisj  3503  undif4  3514  disjssun  3515  sbcssg  3560  eltpg  3668  raltpg  3676  rextpg  3677  r19.12sn  3689  opeq1  3809  opeq2  3810  intmin4  3903  dfiun2g  3949  iindif2m  3985  iinin2m  3986  breq  4036  breq1  4037  breq2  4038  treq  4138  opthg2  4273  poeq1  4335  soeq1  4351  frforeq1  4379  freq1  4380  frforeq2  4381  freq2  4382  frforeq3  4383  weeq1  4392  weeq2  4393  ordeq  4408  limeq  4413  rabxfrd  4505  iunpw  4516  opthprc  4715  releq  4746  sbcrel  4750  eqrel  4753  eqrelrel  4765  xpiindim  4804  brcnvg  4848  brresg  4955  resieq  4957  xpcanm  5110  xpcan2m  5111  dmsnopg  5142  dfco2a  5171  cnvpom  5213  cnvsom  5214  iotaeq  5228  sniota  5250  sbcfung  5283  fneq1  5347  fneq2  5348  feq1  5393  feq2  5394  feq3  5395  sbcfng  5408  sbcfg  5409  f1eq1  5461  f1eq2  5462  f1eq3  5463  foeq1  5479  foeq2  5480  foeq3  5481  f1oeq1  5495  f1oeq2  5496  f1oeq3  5497  fun11iun  5528  mpteqb  5655  dffo3  5712  fmptco  5731  dff13  5818  f1imaeq  5825  f1eqcocnv  5841  fliftcnv  5845  isoeq1  5851  isoeq2  5852  isoeq3  5853  isoeq4  5854  isoeq5  5855  isocnv2  5862  acexmid  5924  fnotovb  5969  mpoeq123  5985  ottposg  6322  dmtpos  6323  smoeq  6357  nnacan  6579  nnmcan  6586  ereq1  6608  ereq2  6609  elecg  6641  ereldm  6646  ixpiinm  6792  enfi  6943  elfi2  7047  fipwssg  7054  ctssdccl  7186  tapeq1  7337  tapeq2  7338  creur  9005  eqreznegel  9707  ltxr  9869  icoshftf1o  10085  elfzm11  10185  elfzomelpfzo  10326  nn0ennn  10544  nnesq  10770  rexfiuz  11173  cau4  11300  sumeq2  11543  fisumcom2  11622  fprodcom2fi  11810  dvdsflip  12035  bitsmod  12140  bitscmp  12142  divgcdcoprm0  12296  hashdvds  12416  4sqlem12  12598  imasaddfnlemg  13018  issgrpv  13108  issgrpn0  13109  mndpropd  13144  ismhm  13165  mhmpropd  13170  issubm2  13177  grppropd  13221  grpinvcnv  13272  conjghm  13484  conjnmzb  13488  ghmpropd  13491  cmnpropd  13503  ablpropd  13504  eqgabl  13538  rngpropd  13589  issrg  13599  ringpropd  13672  crngpropd  13673  opprnzrbg  13819  subrngpropd  13850  resrhm2b  13883  subrgpropd  13887  rhmpropd  13888  opprdomnbg  13908  lmodprop2d  13982  islssm  13991  islssmg  13992  lsspropdg  14065  df2idl2rng  14142  tpspropd  14380  tgss2  14423  lmbr2  14558  txcnmpt  14617  txhmeo  14663  blininf  14768  blres  14778  xmeterval  14779  xmspropd  14821  mspropd  14822  metequiv  14839  xmetxpbl  14852  limcdifap  15006  lgsquadlem1  15426  lgsquadlem2  15427  cbvrald  15542  bj-indeq  15683