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  1322  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  nfbidf  1550  drnf1  1744  drnf2  1745  drsb1  1810  sbal2  2032  eubidh  2044  eubid  2045  mobidh  2072  mobid  2073  eqeq1  2196  eqeq2  2199  eleq1w  2250  eleq2w  2251  eleq1  2252  eleq2  2253  cbvabw  2312  eqabdv  2318  nfceqdf  2331  drnfc1  2349  drnfc2  2350  neeq1  2373  neeq2  2374  neleq1  2459  neleq2  2460  dfrex2dc  2481  ralbida  2484  rexbida  2485  ralbidv2  2492  rexbidv2  2493  ralbid2  2494  rexbid2  2495  r19.21t  2565  r19.23t  2597  reubida  2672  rmobida  2677  raleqf  2682  rexeqf  2683  reueq1f  2684  rmoeq1f  2685  cbvraldva2  2725  cbvrexdva2  2726  dfsbcq  2979  sbceqbid  2984  sbcbi2  3028  sbcbid  3035  eqsbc2  3038  sbcabel  3059  sbnfc2  3132  ssconb  3283  uneq1  3297  ineq1  3344  difin2  3412  reuun2  3433  reldisj  3489  undif4  3500  disjssun  3501  sbcssg  3547  eltpg  3655  raltpg  3663  rextpg  3664  r19.12sn  3676  opeq1  3796  opeq2  3797  intmin4  3890  dfiun2g  3936  iindif2m  3972  iinin2m  3973  breq  4023  breq1  4024  breq2  4025  treq  4125  opthg2  4260  poeq1  4320  soeq1  4336  frforeq1  4364  freq1  4365  frforeq2  4366  freq2  4367  frforeq3  4368  weeq1  4377  weeq2  4378  ordeq  4393  limeq  4398  rabxfrd  4490  iunpw  4501  opthprc  4698  releq  4729  sbcrel  4733  eqrel  4736  eqrelrel  4748  xpiindim  4785  brcnvg  4829  brresg  4936  resieq  4938  xpcanm  5089  xpcan2m  5090  dmsnopg  5121  dfco2a  5150  cnvpom  5192  cnvsom  5193  iotaeq  5207  sniota  5229  sbcfung  5262  fneq1  5326  fneq2  5327  feq1  5370  feq2  5371  feq3  5372  sbcfng  5385  sbcfg  5386  f1eq1  5438  f1eq2  5439  f1eq3  5440  foeq1  5456  foeq2  5457  foeq3  5458  f1oeq1  5471  f1oeq2  5472  f1oeq3  5473  fun11iun  5504  mpteqb  5630  dffo3  5687  fmptco  5706  dff13  5793  f1imaeq  5800  f1eqcocnv  5816  fliftcnv  5820  isoeq1  5826  isoeq2  5827  isoeq3  5828  isoeq4  5829  isoeq5  5830  isocnv2  5837  acexmid  5899  fnotovb  5943  mpoeq123  5959  ottposg  6284  dmtpos  6285  smoeq  6319  nnacan  6541  nnmcan  6548  ereq1  6570  ereq2  6571  elecg  6603  ereldm  6608  ixpiinm  6754  enfi  6905  elfi2  7005  fipwssg  7012  ctssdccl  7144  tapeq1  7286  tapeq2  7287  creur  8952  eqreznegel  9651  ltxr  9812  icoshftf1o  10028  elfzm11  10128  elfzomelpfzo  10268  nn0ennn  10471  nnesq  10681  rexfiuz  11040  cau4  11167  sumeq2  11409  fisumcom2  11488  fprodcom2fi  11676  dvdsflip  11899  divgcdcoprm0  12145  hashdvds  12265  4sqlem12  12446  imasaddfnlemg  12803  issgrpv  12891  issgrpn0  12892  mndpropd  12925  ismhm  12937  mhmpropd  12942  issubm2  12949  grppropd  12986  grpinvcnv  13036  conjghm  13241  conjnmzb  13245  ghmpropd  13248  cmnpropd  13260  ablpropd  13261  eqgabl  13293  rngpropd  13335  issrg  13345  ringpropd  13418  crngpropd  13419  subrngpropd  13589  subrgpropd  13621  lmodprop2d  13690  islssm  13699  islssmg  13700  lsspropdg  13773  df2idl2rng  13849  tpspropd  14022  tgss2  14065  lmbr2  14200  txcnmpt  14259  txhmeo  14305  blininf  14410  blres  14420  xmeterval  14421  xmspropd  14463  mspropd  14464  metequiv  14481  xmetxpbl  14494  limcdifap  14634  cbvrald  15044  bj-indeq  15185