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  11271  cau4  11398  sumeq2  11641  fisumcom2  11720  fprodcom2fi  11908  dvdsflip  12133  bitsmod  12238  bitscmp  12240  divgcdcoprm0  12394  hashdvds  12514  4sqlem12  12696  imasaddfnlemg  13117  issgrpv  13207  issgrpn0  13208  mndpropd  13243  ismhm  13264  mhmpropd  13269  issubm2  13276  grppropd  13320  grpinvcnv  13371  conjghm  13583  conjnmzb  13587  ghmpropd  13590  cmnpropd  13602  ablpropd  13603  eqgabl  13637  rngpropd  13688  issrg  13698  ringpropd  13771  crngpropd  13772  opprnzrbg  13918  subrngpropd  13949  resrhm2b  13982  subrgpropd  13986  rhmpropd  13987  opprdomnbg  14007  lmodprop2d  14081  islssm  14090  islssmg  14091  lsspropdg  14164  df2idl2rng  14241  tpspropd  14479  tgss2  14522  lmbr2  14657  txcnmpt  14716  txhmeo  14762  blininf  14867  blres  14877  xmeterval  14878  xmspropd  14920  mspropd  14921  metequiv  14938  xmetxpbl  14951  limcdifap  15105  lgsquadlem1  15525  lgsquadlem2  15526  cbvrald  15686  bj-indeq  15827