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  791  stbid  832  dcbid  838  pm4.14dc  890  orbididc  953  3orbi123d  1311  3anbi123d  1312  xorbi2d  1380  xorbi1d  1381  nfbidf  1539  drnf1  1733  drnf2  1734  drsb1  1799  sbal2  2020  eubidh  2032  eubid  2033  mobidh  2060  mobid  2061  eqeq1  2184  eqeq2  2187  eleq1w  2238  eleq2w  2239  eleq1  2240  eleq2  2241  cbvabw  2300  nfceqdf  2318  drnfc1  2336  drnfc2  2337  neeq1  2360  neeq2  2361  neleq1  2446  neleq2  2447  dfrex2dc  2468  ralbida  2471  rexbida  2472  ralbidv2  2479  rexbidv2  2480  ralbid2  2481  rexbid2  2482  r19.21t  2552  r19.23t  2584  reubida  2659  rmobida  2664  raleqf  2669  rexeqf  2670  reueq1f  2671  rmoeq1f  2672  cbvraldva2  2712  cbvrexdva2  2713  dfsbcq  2966  sbceqbid  2971  sbcbi2  3015  sbcbid  3022  eqsbc2  3025  sbcabel  3046  sbnfc2  3119  ssconb  3270  uneq1  3284  ineq1  3331  difin2  3399  reuun2  3420  reldisj  3476  undif4  3487  disjssun  3488  sbcssg  3534  eltpg  3639  raltpg  3647  rextpg  3648  r19.12sn  3660  opeq1  3780  opeq2  3781  intmin4  3874  dfiun2g  3920  iindif2m  3956  iinin2m  3957  breq  4007  breq1  4008  breq2  4009  treq  4109  opthg2  4241  poeq1  4301  soeq1  4317  frforeq1  4345  freq1  4346  frforeq2  4347  freq2  4348  frforeq3  4349  weeq1  4358  weeq2  4359  ordeq  4374  limeq  4379  rabxfrd  4471  iunpw  4482  opthprc  4679  releq  4710  sbcrel  4714  eqrel  4717  eqrelrel  4729  xpiindim  4766  brcnvg  4810  brresg  4917  resieq  4919  xpcanm  5070  xpcan2m  5071  dmsnopg  5102  dfco2a  5131  cnvpom  5173  cnvsom  5174  iotaeq  5188  sniota  5209  sbcfung  5242  fneq1  5306  fneq2  5307  feq1  5350  feq2  5351  feq3  5352  sbcfng  5365  sbcfg  5366  f1eq1  5418  f1eq2  5419  f1eq3  5420  foeq1  5436  foeq2  5437  foeq3  5438  f1oeq1  5451  f1oeq2  5452  f1oeq3  5453  fun11iun  5484  mpteqb  5608  dffo3  5665  fmptco  5684  dff13  5771  f1imaeq  5778  f1eqcocnv  5794  fliftcnv  5798  isoeq1  5804  isoeq2  5805  isoeq3  5806  isoeq4  5807  isoeq5  5808  isocnv2  5815  acexmid  5876  fnotovb  5920  mpoeq123  5936  ottposg  6258  dmtpos  6259  smoeq  6293  nnacan  6515  nnmcan  6522  ereq1  6544  ereq2  6545  elecg  6575  ereldm  6580  ixpiinm  6726  enfi  6875  elfi2  6973  fipwssg  6980  ctssdccl  7112  tapeq1  7253  tapeq2  7254  creur  8918  eqreznegel  9616  ltxr  9777  icoshftf1o  9993  elfzm11  10093  elfzomelpfzo  10233  nn0ennn  10435  nnesq  10642  rexfiuz  11000  cau4  11127  sumeq2  11369  fisumcom2  11448  fprodcom2fi  11636  dvdsflip  11859  divgcdcoprm0  12103  hashdvds  12223  imasaddfnlemg  12740  issgrpv  12815  issgrpn0  12816  mndpropd  12846  ismhm  12858  mhmpropd  12862  issubm2  12869  grppropd  12898  grpinvcnv  12943  cmnpropd  13103  ablpropd  13104  issrg  13153  ringpropd  13222  crngpropd  13223  subrgpropd  13374  lmodprop2d  13443  islssm  13450  tpspropd  13575  tgss2  13618  lmbr2  13753  txcnmpt  13812  txhmeo  13858  blininf  13963  blres  13973  xmeterval  13974  xmspropd  14016  mspropd  14017  metequiv  14034  xmetxpbl  14047  limcdifap  14170  cbvrald  14579  bj-indeq  14720