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  1563  drnf1  1757  drnf2  1758  drsb1  1823  sbal2  2049  eubidh  2061  eubid  2062  mobidh  2089  mobid  2090  eqeq1  2213  eqeq2  2216  eleq1w  2267  eleq2w  2268  eleq1  2269  eleq2  2270  cbvabw  2329  eqabdv  2335  nfceqdf  2348  drnfc1  2366  drnfc2  2367  neeq1  2390  neeq2  2391  neleq1  2476  neleq2  2477  dfrex2dc  2498  ralbida  2501  rexbida  2502  ralbidv2  2509  rexbidv2  2510  ralbid2  2511  rexbid2  2512  r19.21t  2582  r19.23t  2614  reubida  2689  rmobida  2694  raleqf  2699  rexeqf  2700  reueq1f  2701  rmoeq1f  2702  cbvraldva2  2746  cbvrexdva2  2747  dfsbcq  3004  sbceqbid  3009  sbcbi2  3053  sbcbid  3060  eqsbc2  3063  sbcabel  3084  sbnfc2  3158  ssconb  3310  uneq1  3324  ineq1  3371  difin2  3439  reuun2  3460  reldisj  3516  undif4  3527  disjssun  3528  sbcssg  3573  eltpg  3683  raltpg  3691  rextpg  3692  r19.12sn  3704  opeq1  3828  opeq2  3829  intmin4  3922  dfiun2g  3968  iindif2m  4004  iinin2m  4005  breq  4056  breq1  4057  breq2  4058  treq  4159  opthg2  4296  poeq1  4359  soeq1  4375  frforeq1  4403  freq1  4404  frforeq2  4405  freq2  4406  frforeq3  4407  weeq1  4416  weeq2  4417  ordeq  4432  limeq  4437  rabxfrd  4529  iunpw  4540  opthprc  4739  releq  4770  sbcrel  4774  eqrel  4777  eqrelrel  4789  xpiindim  4828  brcnvg  4872  brresg  4981  resieq  4983  xpcanm  5136  xpcan2m  5137  dmsnopg  5168  dfco2a  5197  cnvpom  5239  cnvsom  5240  iotaeq  5254  sniota  5276  sbcfung  5309  fneq1  5376  fneq2  5377  feq1  5423  feq2  5424  feq3  5425  sbcfng  5438  sbcfg  5439  f1eq1  5493  f1eq2  5494  f1eq3  5495  foeq1  5511  foeq2  5512  foeq3  5513  f1oeq1  5527  f1oeq2  5528  f1oeq3  5529  fun11iun  5560  mpteqb  5688  dffo3  5745  fmptco  5764  dff13  5855  f1imaeq  5862  f1eqcocnv  5878  fliftcnv  5882  isoeq1  5888  isoeq2  5889  isoeq3  5890  isoeq4  5891  isoeq5  5892  isocnv2  5899  acexmid  5961  fnotovb  6006  mpoeq123  6022  ottposg  6359  dmtpos  6360  smoeq  6394  nnacan  6616  nnmcan  6623  ereq1  6645  ereq2  6646  elecg  6678  ereldm  6683  ixpiinm  6829  enfi  6991  elfi2  7095  fipwssg  7102  ctssdccl  7234  tapeq1  7394  tapeq2  7395  creur  9062  eqreznegel  9765  ltxr  9927  icoshftf1o  10143  elfzm11  10243  elfzomelpfzo  10392  nn0ennn  10610  nnesq  10836  rexfiuz  11385  cau4  11512  sumeq2  11755  fisumcom2  11834  fprodcom2fi  12022  dvdsflip  12247  bitsmod  12352  bitscmp  12354  divgcdcoprm0  12508  hashdvds  12628  4sqlem12  12810  imasaddfnlemg  13231  issgrpv  13321  issgrpn0  13322  mndpropd  13357  ismhm  13378  mhmpropd  13383  issubm2  13390  grppropd  13434  grpinvcnv  13485  conjghm  13697  conjnmzb  13701  ghmpropd  13704  cmnpropd  13716  ablpropd  13717  eqgabl  13751  rngpropd  13802  issrg  13812  ringpropd  13885  crngpropd  13886  opprnzrbg  14032  subrngpropd  14063  resrhm2b  14096  subrgpropd  14100  rhmpropd  14101  opprdomnbg  14121  lmodprop2d  14195  islssm  14204  islssmg  14205  lsspropdg  14278  df2idl2rng  14355  tpspropd  14593  tgss2  14636  lmbr2  14771  txcnmpt  14830  txhmeo  14876  blininf  14981  blres  14991  xmeterval  14992  xmspropd  15034  mspropd  15035  metequiv  15052  xmetxpbl  15065  limcdifap  15219  lgsquadlem1  15639  lgsquadlem2  15640  cbvrald  15894  bj-indeq  16034