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  796  stbid  837  dcbid  843  pm4.14dc  895  orbididc  959  ifpbi123d  998  3orbi123d  1345  3anbi123d  1346  xorbi2d  1422  xorbi1d  1423  nfbidf  1585  drnf1  1779  drnf2  1780  drsb1  1845  sbal2  2071  eubidh  2083  eubid  2084  mobidh  2111  mobid  2112  eqeq1  2236  eqeq2  2239  eleq1w  2290  eleq2w  2291  eleq1  2292  eleq2  2293  cbvabw  2352  eqabdv  2358  nfceqdf  2371  drnfc1  2389  drnfc2  2390  neeq1  2413  neeq2  2414  neleq1  2499  neleq2  2500  dfrex2dc  2521  ralbida  2524  rexbida  2525  ralbidv2  2532  rexbidv2  2533  ralbid2  2534  rexbid2  2535  r19.21t  2605  r19.23t  2638  reubida  2713  rmobida  2719  raleqf  2724  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  cbvraldva2  2772  cbvrexdva2  2773  dfsbcq  3030  sbceqbid  3035  sbcbi2  3079  sbcbid  3086  eqsbc2  3089  sbcabel  3111  sbnfc2  3185  ssconb  3337  uneq1  3351  ineq1  3398  difin2  3466  reuun2  3487  reldisj  3543  undif4  3554  disjssun  3555  sbcssg  3600  eltpg  3711  raltpg  3719  rextpg  3720  r19.12sn  3732  opeq1  3856  opeq2  3857  intmin4  3950  dfiun2g  3996  iindif2m  4032  iinin2m  4033  breq  4084  breq1  4085  breq2  4086  treq  4187  opthg2  4324  poeq1  4389  soeq1  4405  frforeq1  4433  freq1  4434  frforeq2  4435  freq2  4436  frforeq3  4437  weeq1  4446  weeq2  4447  ordeq  4462  limeq  4467  rabxfrd  4559  iunpw  4570  opthprc  4769  releq  4800  sbcrel  4804  eqrel  4807  eqrelrel  4819  xpiindim  4858  brcnvg  4902  brresg  5012  resieq  5014  xpcanm  5167  xpcan2m  5168  dmsnopg  5199  dfco2a  5228  cnvpom  5270  cnvsom  5271  iotaeq  5286  sniota  5308  sbcfung  5341  fneq1  5408  fneq2  5409  feq1  5455  feq2  5456  feq3  5457  sbcfng  5470  sbcfg  5471  f1eq1  5525  f1eq2  5526  f1eq3  5527  foeq1  5543  foeq2  5544  foeq3  5545  f1oeq1  5559  f1oeq2  5560  f1oeq3  5561  fun11iun  5592  mpteqb  5724  dffo3  5781  fmptco  5800  dff13  5891  f1imaeq  5898  f1eqcocnv  5914  fliftcnv  5918  isoeq1  5924  isoeq2  5925  isoeq3  5926  isoeq4  5927  isoeq5  5928  isocnv2  5935  acexmid  5999  fnotovb  6046  mpoeq123  6062  ottposg  6399  dmtpos  6400  smoeq  6434  nnacan  6656  nnmcan  6663  ereq1  6685  ereq2  6686  elecg  6718  ereldm  6723  ixpiinm  6869  enfi  7031  elfi2  7135  fipwssg  7142  ctssdccl  7274  tapeq1  7434  tapeq2  7435  creur  9102  eqreznegel  9805  ltxr  9967  icoshftf1o  10183  elfzm11  10283  elfzomelpfzo  10432  nn0ennn  10650  nnesq  10876  rexfiuz  11495  cau4  11622  sumeq2  11865  fisumcom2  11944  fprodcom2fi  12132  dvdsflip  12357  bitsmod  12462  bitscmp  12464  divgcdcoprm0  12618  hashdvds  12738  4sqlem12  12920  imasaddfnlemg  13342  issgrpv  13432  issgrpn0  13433  mndpropd  13468  ismhm  13489  mhmpropd  13494  issubm2  13501  grppropd  13545  grpinvcnv  13596  conjghm  13808  conjnmzb  13812  ghmpropd  13815  cmnpropd  13827  ablpropd  13828  eqgabl  13862  rngpropd  13913  issrg  13923  ringpropd  13996  crngpropd  13997  opprnzrbg  14143  subrngpropd  14174  resrhm2b  14207  subrgpropd  14211  rhmpropd  14212  opprdomnbg  14232  lmodprop2d  14306  islssm  14315  islssmg  14316  lsspropdg  14389  df2idl2rng  14466  tpspropd  14704  tgss2  14747  lmbr2  14882  txcnmpt  14941  txhmeo  14987  blininf  15092  blres  15102  xmeterval  15103  xmspropd  15145  mspropd  15146  metequiv  15163  xmetxpbl  15176  limcdifap  15330  lgsquadlem1  15750  lgsquadlem2  15751  ushgredgedg  16018  ushgredgedgloop  16020  cbvrald  16110  bj-indeq  16250