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  799  stbid  840  dcbid  846  pm4.14dc  898  orbididc  962  ifpbi123d  1001  3orbi123d  1348  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  nfbidf  1588  drnf1  1782  drnf2  1783  drsb1  1848  sbal2  2074  eubidh  2086  eubid  2087  mobidh  2114  mobid  2115  eqeq1  2239  eqeq2  2242  eleq1w  2293  eleq2w  2294  eleq1  2295  eleq2  2296  abbi  2351  cbvabw  2357  eqabdv  2363  nfceqdf  2383  drnfc1  2401  drnfc2  2402  neeq1  2425  neeq2  2426  neleq1  2511  neleq2  2512  dfrex2dc  2533  ralbida  2536  rexbida  2537  ralbidv2  2544  rexbidv2  2545  ralbid2  2546  rexbid2  2547  r19.21t  2617  r19.23t  2650  reubida  2726  rmobida  2732  raleqf  2737  rexeqf  2738  reueq1f  2739  rmoeq1f  2740  cbvraldva2  2785  cbvrexdva2  2786  dfsbcq  3044  sbceqbid  3049  sbcbi2  3093  sbcbid  3100  eqsbc2  3103  sbcabel  3125  sbnfc2  3199  ssconb  3352  uneq1  3366  ineq1  3415  difin2  3483  reuun2  3504  reldisj  3560  undif4  3571  disjssun  3572  sbcssg  3618  eltpg  3734  raltpg  3742  rextpg  3743  r19.12sn  3755  opeq1  3883  opeq2  3884  intmin4  3977  dfiun2g  4023  iindif2m  4059  iinin2m  4060  breq  4111  breq1  4112  breq2  4113  treq  4214  opthg2  4355  poeq1  4420  soeq1  4436  frforeq1  4464  freq1  4465  frforeq2  4466  freq2  4467  frforeq3  4468  weeq1  4477  weeq2  4478  ordeq  4493  limeq  4498  rabxfrd  4590  iunpw  4601  opthprc  4801  releq  4832  sbcrel  4836  eqrel  4839  eqrelrel  4851  xpiindim  4892  brcnvg  4936  brresg  5046  resieq  5048  xpcanm  5202  xpcan2m  5203  dmsnopg  5234  dfco2a  5263  cnvpom  5305  cnvsom  5306  iotaeq  5321  sniota  5343  sbcfung  5376  fneq1  5444  fneq2  5445  feq1  5491  feq2  5492  feq3  5493  sbcfng  5506  sbcfg  5507  f1eq1  5568  f1eq2  5569  f1eq3  5570  foeq1  5586  foeq2  5587  foeq3  5588  f1oeq1  5602  f1oeq2  5603  f1oeq3  5604  fun11iun  5635  mpteqb  5768  dffo3  5824  fmptco  5843  dff13  5941  f1imaeq  5948  f1eqcocnv  5964  fliftcnv  5968  isoeq1  5974  isoeq2  5975  isoeq3  5976  isoeq4  5977  isoeq5  5978  isocnv2  5985  acexmid  6049  fnotovb  6096  mpoeq123  6112  ottposg  6486  dmtpos  6487  smoeq  6521  nnacan  6745  nnmcan  6752  ereq1  6774  ereq2  6775  elecg  6807  ereldm  6812  ixpiinm  6959  enfi  7128  elfi2  7259  fipwssg  7266  ctssdccl  7402  tapeq1  7566  tapeq2  7567  creur  9233  eqreznegel  9946  ltxr  10108  icoshftf1o  10324  elfzm11  10425  elfzomelpfzo  10576  nn0ennn  10795  nnesq  11021  rexfiuz  11674  cau4  11801  sumeq2  12044  fisumcom2  12124  fprodcom2fi  12312  dvdsflip  12537  bitsmod  12642  bitscmp  12644  divgcdcoprm0  12798  hashdvds  12918  4sqlem12  13100  imasaddfnlemg  13527  issgrpv  13617  issgrpn0  13618  mndpropd  13653  ismhm  13674  mhmpropd  13679  issubm2  13686  grppropd  13730  grpinvcnv  13781  conjghm  13993  conjnmzb  13997  ghmpropd  14000  cmnpropd  14012  ablpropd  14013  eqgabl  14047  rngpropd  14099  issrg  14109  ringpropd  14182  crngpropd  14183  opprnzrbg  14330  subrngpropd  14361  resrhm2b  14394  subrgpropd  14398  rhmpropd  14399  opprdomnbg  14420  lmodprop2d  14496  islssm  14505  islssmg  14506  lsspropdg  14579  df2idl2rng  14656  psrbagconf1o  14828  tpspropd  14901  tgss2  14944  lmbr2  15079  txcnmpt  15138  txhmeo  15184  blininf  15289  blres  15299  xmeterval  15300  xmspropd  15342  mspropd  15343  metequiv  15360  xmetxpbl  15373  limcdifap  15527  lgsquadlem1  15950  lgsquadlem2  15951  ushgredgedg  16221  ushgredgedgloop  16223  upgriswlkdc  16355  clwwlknonel  16427  eupth2lem2dc  16454  cbvrald  16560  bj-indeq  16699