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  798  stbid  839  dcbid  845  pm4.14dc  897  orbididc  961  ifpbi123d  1000  3orbi123d  1347  3anbi123d  1348  xorbi2d  1424  xorbi1d  1425  nfbidf  1587  drnf1  1781  drnf2  1782  drsb1  1847  sbal2  2073  eubidh  2085  eubid  2086  mobidh  2113  mobid  2114  eqeq1  2238  eqeq2  2241  eleq1w  2292  eleq2w  2293  eleq1  2294  eleq2  2295  cbvabw  2354  eqabdv  2360  nfceqdf  2373  drnfc1  2391  drnfc2  2392  neeq1  2415  neeq2  2416  neleq1  2501  neleq2  2502  dfrex2dc  2523  ralbida  2526  rexbida  2527  ralbidv2  2534  rexbidv2  2535  ralbid2  2536  rexbid2  2537  r19.21t  2607  r19.23t  2640  reubida  2715  rmobida  2721  raleqf  2726  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  cbvraldva2  2774  cbvrexdva2  2775  dfsbcq  3033  sbceqbid  3038  sbcbi2  3082  sbcbid  3089  eqsbc2  3092  sbcabel  3114  sbnfc2  3188  ssconb  3340  uneq1  3354  ineq1  3401  difin2  3469  reuun2  3490  reldisj  3546  undif4  3557  disjssun  3558  sbcssg  3603  eltpg  3714  raltpg  3722  rextpg  3723  r19.12sn  3735  opeq1  3862  opeq2  3863  intmin4  3956  dfiun2g  4002  iindif2m  4038  iinin2m  4039  breq  4090  breq1  4091  breq2  4092  treq  4193  opthg2  4331  poeq1  4396  soeq1  4412  frforeq1  4440  freq1  4441  frforeq2  4442  freq2  4443  frforeq3  4444  weeq1  4453  weeq2  4454  ordeq  4469  limeq  4474  rabxfrd  4566  iunpw  4577  opthprc  4777  releq  4808  sbcrel  4812  eqrel  4815  eqrelrel  4827  xpiindim  4867  brcnvg  4911  brresg  5021  resieq  5023  xpcanm  5176  xpcan2m  5177  dmsnopg  5208  dfco2a  5237  cnvpom  5279  cnvsom  5280  iotaeq  5295  sniota  5317  sbcfung  5350  fneq1  5418  fneq2  5419  feq1  5465  feq2  5466  feq3  5467  sbcfng  5480  sbcfg  5481  f1eq1  5537  f1eq2  5538  f1eq3  5539  foeq1  5555  foeq2  5556  foeq3  5557  f1oeq1  5571  f1oeq2  5572  f1oeq3  5573  fun11iun  5604  mpteqb  5737  dffo3  5794  fmptco  5813  dff13  5909  f1imaeq  5916  f1eqcocnv  5932  fliftcnv  5936  isoeq1  5942  isoeq2  5943  isoeq3  5944  isoeq4  5945  isoeq5  5946  isocnv2  5953  acexmid  6017  fnotovb  6064  mpoeq123  6080  ottposg  6421  dmtpos  6422  smoeq  6456  nnacan  6680  nnmcan  6687  ereq1  6709  ereq2  6710  elecg  6742  ereldm  6747  ixpiinm  6893  enfi  7060  elfi2  7171  fipwssg  7178  ctssdccl  7310  tapeq1  7471  tapeq2  7472  creur  9139  eqreznegel  9848  ltxr  10010  icoshftf1o  10226  elfzm11  10326  elfzomelpfzo  10477  nn0ennn  10696  nnesq  10922  rexfiuz  11554  cau4  11681  sumeq2  11924  fisumcom2  12004  fprodcom2fi  12192  dvdsflip  12417  bitsmod  12522  bitscmp  12524  divgcdcoprm0  12678  hashdvds  12798  4sqlem12  12980  imasaddfnlemg  13402  issgrpv  13492  issgrpn0  13493  mndpropd  13528  ismhm  13549  mhmpropd  13554  issubm2  13561  grppropd  13605  grpinvcnv  13656  conjghm  13868  conjnmzb  13872  ghmpropd  13875  cmnpropd  13887  ablpropd  13888  eqgabl  13922  rngpropd  13974  issrg  13984  ringpropd  14057  crngpropd  14058  opprnzrbg  14205  subrngpropd  14236  resrhm2b  14269  subrgpropd  14273  rhmpropd  14274  opprdomnbg  14294  lmodprop2d  14368  islssm  14377  islssmg  14378  lsspropdg  14451  df2idl2rng  14528  tpspropd  14766  tgss2  14809  lmbr2  14944  txcnmpt  15003  txhmeo  15049  blininf  15154  blres  15164  xmeterval  15165  xmspropd  15207  mspropd  15208  metequiv  15225  xmetxpbl  15238  limcdifap  15392  lgsquadlem1  15812  lgsquadlem2  15813  ushgredgedg  16083  ushgredgedgloop  16085  upgriswlkdc  16217  clwwlknonel  16289  eupth2lem2dc  16316  cbvrald  16410  bj-indeq  16550