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  5908  f1imaeq  5915  f1eqcocnv  5931  fliftcnv  5935  isoeq1  5941  isoeq2  5942  isoeq3  5943  isoeq4  5944  isoeq5  5945  isocnv2  5952  acexmid  6016  fnotovb  6063  mpoeq123  6079  ottposg  6420  dmtpos  6421  smoeq  6455  nnacan  6679  nnmcan  6686  ereq1  6708  ereq2  6709  elecg  6741  ereldm  6746  ixpiinm  6892  enfi  7059  elfi2  7170  fipwssg  7177  ctssdccl  7309  tapeq1  7470  tapeq2  7471  creur  9138  eqreznegel  9847  ltxr  10009  icoshftf1o  10225  elfzm11  10325  elfzomelpfzo  10475  nn0ennn  10694  nnesq  10920  rexfiuz  11549  cau4  11676  sumeq2  11919  fisumcom2  11998  fprodcom2fi  12186  dvdsflip  12411  bitsmod  12516  bitscmp  12518  divgcdcoprm0  12672  hashdvds  12792  4sqlem12  12974  imasaddfnlemg  13396  issgrpv  13486  issgrpn0  13487  mndpropd  13522  ismhm  13543  mhmpropd  13548  issubm2  13555  grppropd  13599  grpinvcnv  13650  conjghm  13862  conjnmzb  13866  ghmpropd  13869  cmnpropd  13881  ablpropd  13882  eqgabl  13916  rngpropd  13967  issrg  13977  ringpropd  14050  crngpropd  14051  opprnzrbg  14198  subrngpropd  14229  resrhm2b  14262  subrgpropd  14266  rhmpropd  14267  opprdomnbg  14287  lmodprop2d  14361  islssm  14370  islssmg  14371  lsspropdg  14444  df2idl2rng  14521  tpspropd  14759  tgss2  14802  lmbr2  14937  txcnmpt  14996  txhmeo  15042  blininf  15147  blres  15157  xmeterval  15158  xmspropd  15200  mspropd  15201  metequiv  15218  xmetxpbl  15231  limcdifap  15385  lgsquadlem1  15805  lgsquadlem2  15806  ushgredgedg  16076  ushgredgedgloop  16078  upgriswlkdc  16210  clwwlknonel  16282  eupth2lem2dc  16309  cbvrald  16384  bj-indeq  16524