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  793  stbid  834  dcbid  840  pm4.14dc  892  orbididc  956  3orbi123d  1324  3anbi123d  1325  xorbi2d  1400  xorbi1d  1401  nfbidf  1562  drnf1  1756  drnf2  1757  drsb1  1822  sbal2  2048  eubidh  2060  eubid  2061  mobidh  2088  mobid  2089  eqeq1  2212  eqeq2  2215  eleq1w  2266  eleq2w  2267  eleq1  2268  eleq2  2269  cbvabw  2328  eqabdv  2334  nfceqdf  2347  drnfc1  2365  drnfc2  2366  neeq1  2389  neeq2  2390  neleq1  2475  neleq2  2476  dfrex2dc  2497  ralbida  2500  rexbida  2501  ralbidv2  2508  rexbidv2  2509  ralbid2  2510  rexbid2  2511  r19.21t  2581  r19.23t  2613  reubida  2688  rmobida  2693  raleqf  2698  rexeqf  2699  reueq1f  2700  rmoeq1f  2701  cbvraldva2  2745  cbvrexdva2  2746  dfsbcq  3000  sbceqbid  3005  sbcbi2  3049  sbcbid  3056  eqsbc2  3059  sbcabel  3080  sbnfc2  3154  ssconb  3306  uneq1  3320  ineq1  3367  difin2  3435  reuun2  3456  reldisj  3512  undif4  3523  disjssun  3524  sbcssg  3569  eltpg  3678  raltpg  3686  rextpg  3687  r19.12sn  3699  opeq1  3819  opeq2  3820  intmin4  3913  dfiun2g  3959  iindif2m  3995  iinin2m  3996  breq  4046  breq1  4047  breq2  4048  treq  4148  opthg2  4283  poeq1  4346  soeq1  4362  frforeq1  4390  freq1  4391  frforeq2  4392  freq2  4393  frforeq3  4394  weeq1  4403  weeq2  4404  ordeq  4419  limeq  4424  rabxfrd  4516  iunpw  4527  opthprc  4726  releq  4757  sbcrel  4761  eqrel  4764  eqrelrel  4776  xpiindim  4815  brcnvg  4859  brresg  4967  resieq  4969  xpcanm  5122  xpcan2m  5123  dmsnopg  5154  dfco2a  5183  cnvpom  5225  cnvsom  5226  iotaeq  5240  sniota  5262  sbcfung  5295  fneq1  5362  fneq2  5363  feq1  5408  feq2  5409  feq3  5410  sbcfng  5423  sbcfg  5424  f1eq1  5476  f1eq2  5477  f1eq3  5478  foeq1  5494  foeq2  5495  foeq3  5496  f1oeq1  5510  f1oeq2  5511  f1oeq3  5512  fun11iun  5543  mpteqb  5670  dffo3  5727  fmptco  5746  dff13  5837  f1imaeq  5844  f1eqcocnv  5860  fliftcnv  5864  isoeq1  5870  isoeq2  5871  isoeq3  5872  isoeq4  5873  isoeq5  5874  isocnv2  5881  acexmid  5943  fnotovb  5988  mpoeq123  6004  ottposg  6341  dmtpos  6342  smoeq  6376  nnacan  6598  nnmcan  6605  ereq1  6627  ereq2  6628  elecg  6660  ereldm  6665  ixpiinm  6811  enfi  6970  elfi2  7074  fipwssg  7081  ctssdccl  7213  tapeq1  7364  tapeq2  7365  creur  9032  eqreznegel  9735  ltxr  9897  icoshftf1o  10113  elfzm11  10213  elfzomelpfzo  10360  nn0ennn  10578  nnesq  10804  rexfiuz  11300  cau4  11427  sumeq2  11670  fisumcom2  11749  fprodcom2fi  11937  dvdsflip  12162  bitsmod  12267  bitscmp  12269  divgcdcoprm0  12423  hashdvds  12543  4sqlem12  12725  imasaddfnlemg  13146  issgrpv  13236  issgrpn0  13237  mndpropd  13272  ismhm  13293  mhmpropd  13298  issubm2  13305  grppropd  13349  grpinvcnv  13400  conjghm  13612  conjnmzb  13616  ghmpropd  13619  cmnpropd  13631  ablpropd  13632  eqgabl  13666  rngpropd  13717  issrg  13727  ringpropd  13800  crngpropd  13801  opprnzrbg  13947  subrngpropd  13978  resrhm2b  14011  subrgpropd  14015  rhmpropd  14016  opprdomnbg  14036  lmodprop2d  14110  islssm  14119  islssmg  14120  lsspropdg  14193  df2idl2rng  14270  tpspropd  14508  tgss2  14551  lmbr2  14686  txcnmpt  14745  txhmeo  14791  blininf  14896  blres  14906  xmeterval  14907  xmspropd  14949  mspropd  14950  metequiv  14967  xmetxpbl  14980  limcdifap  15134  lgsquadlem1  15554  lgsquadlem2  15555  cbvrald  15724  bj-indeq  15865