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  1323  3anbi123d  1324  xorbi2d  1399  xorbi1d  1400  nfbidf  1561  drnf1  1755  drnf2  1756  drsb1  1821  sbal2  2047  eubidh  2059  eubid  2060  mobidh  2087  mobid  2088  eqeq1  2211  eqeq2  2214  eleq1w  2265  eleq2w  2266  eleq1  2267  eleq2  2268  cbvabw  2327  eqabdv  2333  nfceqdf  2346  drnfc1  2364  drnfc2  2365  neeq1  2388  neeq2  2389  neleq1  2474  neleq2  2475  dfrex2dc  2496  ralbida  2499  rexbida  2500  ralbidv2  2507  rexbidv2  2508  ralbid2  2509  rexbid2  2510  r19.21t  2580  r19.23t  2612  reubida  2687  rmobida  2692  raleqf  2697  rexeqf  2698  reueq1f  2699  rmoeq1f  2700  cbvraldva2  2744  cbvrexdva2  2745  dfsbcq  2999  sbceqbid  3004  sbcbi2  3048  sbcbid  3055  eqsbc2  3058  sbcabel  3079  sbnfc2  3153  ssconb  3305  uneq1  3319  ineq1  3366  difin2  3434  reuun2  3455  reldisj  3511  undif4  3522  disjssun  3523  sbcssg  3568  eltpg  3677  raltpg  3685  rextpg  3686  r19.12sn  3698  opeq1  3818  opeq2  3819  intmin4  3912  dfiun2g  3958  iindif2m  3994  iinin2m  3995  breq  4045  breq1  4046  breq2  4047  treq  4147  opthg2  4282  poeq1  4345  soeq1  4361  frforeq1  4389  freq1  4390  frforeq2  4391  freq2  4392  frforeq3  4393  weeq1  4402  weeq2  4403  ordeq  4418  limeq  4423  rabxfrd  4515  iunpw  4526  opthprc  4725  releq  4756  sbcrel  4760  eqrel  4763  eqrelrel  4775  xpiindim  4814  brcnvg  4858  brresg  4966  resieq  4968  xpcanm  5121  xpcan2m  5122  dmsnopg  5153  dfco2a  5182  cnvpom  5224  cnvsom  5225  iotaeq  5239  sniota  5261  sbcfung  5294  fneq1  5361  fneq2  5362  feq1  5407  feq2  5408  feq3  5409  sbcfng  5422  sbcfg  5423  f1eq1  5475  f1eq2  5476  f1eq3  5477  foeq1  5493  foeq2  5494  foeq3  5495  f1oeq1  5509  f1oeq2  5510  f1oeq3  5511  fun11iun  5542  mpteqb  5669  dffo3  5726  fmptco  5745  dff13  5836  f1imaeq  5843  f1eqcocnv  5859  fliftcnv  5863  isoeq1  5869  isoeq2  5870  isoeq3  5871  isoeq4  5872  isoeq5  5873  isocnv2  5880  acexmid  5942  fnotovb  5987  mpoeq123  6003  ottposg  6340  dmtpos  6341  smoeq  6375  nnacan  6597  nnmcan  6604  ereq1  6626  ereq2  6627  elecg  6659  ereldm  6664  ixpiinm  6810  enfi  6969  elfi2  7073  fipwssg  7080  ctssdccl  7212  tapeq1  7363  tapeq2  7364  creur  9031  eqreznegel  9734  ltxr  9896  icoshftf1o  10112  elfzm11  10212  elfzomelpfzo  10358  nn0ennn  10576  nnesq  10802  rexfiuz  11242  cau4  11369  sumeq2  11612  fisumcom2  11691  fprodcom2fi  11879  dvdsflip  12104  bitsmod  12209  bitscmp  12211  divgcdcoprm0  12365  hashdvds  12485  4sqlem12  12667  imasaddfnlemg  13088  issgrpv  13178  issgrpn0  13179  mndpropd  13214  ismhm  13235  mhmpropd  13240  issubm2  13247  grppropd  13291  grpinvcnv  13342  conjghm  13554  conjnmzb  13558  ghmpropd  13561  cmnpropd  13573  ablpropd  13574  eqgabl  13608  rngpropd  13659  issrg  13669  ringpropd  13742  crngpropd  13743  opprnzrbg  13889  subrngpropd  13920  resrhm2b  13953  subrgpropd  13957  rhmpropd  13958  opprdomnbg  13978  lmodprop2d  14052  islssm  14061  islssmg  14062  lsspropdg  14135  df2idl2rng  14212  tpspropd  14450  tgss2  14493  lmbr2  14628  txcnmpt  14687  txhmeo  14733  blininf  14838  blres  14848  xmeterval  14849  xmspropd  14891  mspropd  14892  metequiv  14909  xmetxpbl  14922  limcdifap  15076  lgsquadlem1  15496  lgsquadlem2  15497  cbvrald  15657  bj-indeq  15798