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  2988  sbceqbid  2993  sbcbi2  3037  sbcbid  3044  eqsbc2  3047  sbcabel  3068  sbnfc2  3142  ssconb  3293  uneq1  3307  ineq1  3354  difin2  3422  reuun2  3443  reldisj  3499  undif4  3510  disjssun  3511  sbcssg  3556  eltpg  3664  raltpg  3672  rextpg  3673  r19.12sn  3685  opeq1  3805  opeq2  3806  intmin4  3899  dfiun2g  3945  iindif2m  3981  iinin2m  3982  breq  4032  breq1  4033  breq2  4034  treq  4134  opthg2  4269  poeq1  4331  soeq1  4347  frforeq1  4375  freq1  4376  frforeq2  4377  freq2  4378  frforeq3  4379  weeq1  4388  weeq2  4389  ordeq  4404  limeq  4409  rabxfrd  4501  iunpw  4512  opthprc  4711  releq  4742  sbcrel  4746  eqrel  4749  eqrelrel  4761  xpiindim  4800  brcnvg  4844  brresg  4951  resieq  4953  xpcanm  5106  xpcan2m  5107  dmsnopg  5138  dfco2a  5167  cnvpom  5209  cnvsom  5210  iotaeq  5224  sniota  5246  sbcfung  5279  fneq1  5343  fneq2  5344  feq1  5387  feq2  5388  feq3  5389  sbcfng  5402  sbcfg  5403  f1eq1  5455  f1eq2  5456  f1eq3  5457  foeq1  5473  foeq2  5474  foeq3  5475  f1oeq1  5489  f1oeq2  5490  f1oeq3  5491  fun11iun  5522  mpteqb  5649  dffo3  5706  fmptco  5725  dff13  5812  f1imaeq  5819  f1eqcocnv  5835  fliftcnv  5839  isoeq1  5845  isoeq2  5846  isoeq3  5847  isoeq4  5848  isoeq5  5849  isocnv2  5856  acexmid  5918  fnotovb  5962  mpoeq123  5978  ottposg  6310  dmtpos  6311  smoeq  6345  nnacan  6567  nnmcan  6574  ereq1  6596  ereq2  6597  elecg  6629  ereldm  6634  ixpiinm  6780  enfi  6931  elfi2  7033  fipwssg  7040  ctssdccl  7172  tapeq1  7314  tapeq2  7315  creur  8980  eqreznegel  9682  ltxr  9844  icoshftf1o  10060  elfzm11  10160  elfzomelpfzo  10301  nn0ennn  10507  nnesq  10733  rexfiuz  11136  cau4  11263  sumeq2  11505  fisumcom2  11584  fprodcom2fi  11772  dvdsflip  11996  divgcdcoprm0  12242  hashdvds  12362  4sqlem12  12543  imasaddfnlemg  12900  issgrpv  12990  issgrpn0  12991  mndpropd  13024  ismhm  13036  mhmpropd  13041  issubm2  13048  grppropd  13092  grpinvcnv  13143  conjghm  13349  conjnmzb  13353  ghmpropd  13356  cmnpropd  13368  ablpropd  13369  eqgabl  13403  rngpropd  13454  issrg  13464  ringpropd  13537  crngpropd  13538  opprnzrbg  13684  subrngpropd  13715  resrhm2b  13748  subrgpropd  13752  rhmpropd  13753  opprdomnbg  13773  lmodprop2d  13847  islssm  13856  islssmg  13857  lsspropdg  13930  df2idl2rng  14007  tpspropd  14215  tgss2  14258  lmbr2  14393  txcnmpt  14452  txhmeo  14498  blininf  14603  blres  14613  xmeterval  14614  xmspropd  14656  mspropd  14657  metequiv  14674  xmetxpbl  14687  limcdifap  14841  lgsquadlem1  15234  lgsquadlem2  15235  cbvrald  15350  bj-indeq  15491