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  2036  eubidh  2048  eubid  2049  mobidh  2076  mobid  2077  eqeq1  2200  eqeq2  2203  eleq1w  2254  eleq2w  2255  eleq1  2256  eleq2  2257  cbvabw  2316  eqabdv  2322  nfceqdf  2335  drnfc1  2353  drnfc2  2354  neeq1  2377  neeq2  2378  neleq1  2463  neleq2  2464  dfrex2dc  2485  ralbida  2488  rexbida  2489  ralbidv2  2496  rexbidv2  2497  ralbid2  2498  rexbid2  2499  r19.21t  2569  r19.23t  2601  reubida  2676  rmobida  2681  raleqf  2686  rexeqf  2687  reueq1f  2688  rmoeq1f  2689  cbvraldva2  2733  cbvrexdva2  2734  dfsbcq  2987  sbceqbid  2992  sbcbi2  3036  sbcbid  3043  eqsbc2  3046  sbcabel  3067  sbnfc2  3141  ssconb  3292  uneq1  3306  ineq1  3353  difin2  3421  reuun2  3442  reldisj  3498  undif4  3509  disjssun  3510  sbcssg  3555  eltpg  3663  raltpg  3671  rextpg  3672  r19.12sn  3684  opeq1  3804  opeq2  3805  intmin4  3898  dfiun2g  3944  iindif2m  3980  iinin2m  3981  breq  4031  breq1  4032  breq2  4033  treq  4133  opthg2  4268  poeq1  4330  soeq1  4346  frforeq1  4374  freq1  4375  frforeq2  4376  freq2  4377  frforeq3  4378  weeq1  4387  weeq2  4388  ordeq  4403  limeq  4408  rabxfrd  4500  iunpw  4511  opthprc  4710  releq  4741  sbcrel  4745  eqrel  4748  eqrelrel  4760  xpiindim  4799  brcnvg  4843  brresg  4950  resieq  4952  xpcanm  5105  xpcan2m  5106  dmsnopg  5137  dfco2a  5166  cnvpom  5208  cnvsom  5209  iotaeq  5223  sniota  5245  sbcfung  5278  fneq1  5342  fneq2  5343  feq1  5386  feq2  5387  feq3  5388  sbcfng  5401  sbcfg  5402  f1eq1  5454  f1eq2  5455  f1eq3  5456  foeq1  5472  foeq2  5473  foeq3  5474  f1oeq1  5488  f1oeq2  5489  f1oeq3  5490  fun11iun  5521  mpteqb  5648  dffo3  5705  fmptco  5724  dff13  5811  f1imaeq  5818  f1eqcocnv  5834  fliftcnv  5838  isoeq1  5844  isoeq2  5845  isoeq3  5846  isoeq4  5847  isoeq5  5848  isocnv2  5855  acexmid  5917  fnotovb  5961  mpoeq123  5977  ottposg  6308  dmtpos  6309  smoeq  6343  nnacan  6565  nnmcan  6572  ereq1  6594  ereq2  6595  elecg  6627  ereldm  6632  ixpiinm  6778  enfi  6929  elfi2  7031  fipwssg  7038  ctssdccl  7170  tapeq1  7312  tapeq2  7313  creur  8978  eqreznegel  9679  ltxr  9841  icoshftf1o  10057  elfzm11  10157  elfzomelpfzo  10298  nn0ennn  10504  nnesq  10730  rexfiuz  11133  cau4  11260  sumeq2  11502  fisumcom2  11581  fprodcom2fi  11769  dvdsflip  11993  divgcdcoprm0  12239  hashdvds  12359  4sqlem12  12540  imasaddfnlemg  12897  issgrpv  12987  issgrpn0  12988  mndpropd  13021  ismhm  13033  mhmpropd  13038  issubm2  13045  grppropd  13089  grpinvcnv  13140  conjghm  13346  conjnmzb  13350  ghmpropd  13353  cmnpropd  13365  ablpropd  13366  eqgabl  13400  rngpropd  13451  issrg  13461  ringpropd  13534  crngpropd  13535  opprnzrbg  13681  subrngpropd  13712  resrhm2b  13745  subrgpropd  13749  rhmpropd  13750  opprdomnbg  13770  lmodprop2d  13844  islssm  13853  islssmg  13854  lsspropdg  13927  df2idl2rng  14004  tpspropd  14204  tgss2  14247  lmbr2  14382  txcnmpt  14441  txhmeo  14487  blininf  14592  blres  14602  xmeterval  14603  xmspropd  14645  mspropd  14646  metequiv  14663  xmetxpbl  14676  limcdifap  14816  lgsquadlem1  15191  cbvrald  15280  bj-indeq  15421