Theorem 3bitr4g 313

Description: More general version of 3bitr4i 302. Useful for converting definitions in a formula. (Contributed by NM, 11-May-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	syl5bb 282	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 288	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  bibi1d  343  pm5.32rd  577  orbi2d  912  orbi1d  913  ifpbi123d  1076  ifpbi123dOLD  1077  3orbi123d  1433  3anbi123d  1434  nanbi1  1493  nanbi2  1494  xorbi12d  1519  hadbi123d  1597  had0  1607  cadbi123d  1613  nfbiit  1854  nfbidv  1926  sbequ  2087  nfbidf  2220  drex1v  2369  drnf1v  2370  drnf1vOLD  2371  drex1  2441  drnf1  2443  sb4b  2475  sb4bOLD  2476  drsb1  2499  eujustALT  2572  eubi  2584  eleq1ab  2717  eqeq1d  2740  eqeq1dALT  2741  eqeq2d  2749  abbi1  2807  eleq1w  2821  eleq2w  2822  eleq1d  2823  eleq2d  2824  eleq2dALT  2825  abbi2dv  2876  nfceqdf  2901  nfceqdfOLD  2902  drnfc1  2925  drnfc1OLD  2926  drnfc2  2927  drnfc2OLD  2928  neleq12d  3052  ralbidv2  3118  r19.21t  3137  ralbidaOLD  3157  rexbidv2  3223  r19.23t  3241  rexbida  3246  ralrexbidOLD  3251  ralcom2  3288  reubida  3313  reubidva  3314  rmobida  3318  raleqf  3323  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  raleqbidvv  3329  reueq1  3335  rmoeq1  3336  cbvraldva2  3381  cbvrexdva2  3382  dfsbcq  3713  sbceqbid  3718  sbcbid  3769  sbcbi2  3774  eqsbc2  3781  sbcrext  3802  sbcabel  3807  ss2abdv  3993  psseq1  4018  psseq2  4019  ssconb  4068  uneq1  4086  difin2  4222  rcompleq  4226  reuun2  4245  sbcnel12g  4342  sbnfc2  4367  reldisj  4382  reldisjOLD  4383  undif4  4397  disjssun  4398  pssdifcom1  4417  pssdifcom2  4418  sbcssg  4451  eltpg  4618  raltpg  4631  rextpg  4632  r19.12sn  4653  intmin4  4905  dfiun2g  4957  iindif1  5000  iindif2  5002  iinin2  5003  disjprgw  5065  disjprg  5066  disjxun  5068  breq  5072  breq1  5073  breq2  5074  treq  5193  reusv2lem5  5320  rexxfrd  5327  rexxfr2d  5329  rexxfrd2  5331  rabxfrd  5335  opthg2  5388  oteqex2  5407  oteqex  5408  poeq1  5497  soeq1  5515  freq1  5550  weeq1  5568  weeq2  5569  opthprc  5642  wesn  5666  releq  5677  sbcrel  5681  eqrel  5684  eqrelrel  5696  xpiindi  5733  dmopab2rex  5815  dfres3  5885  brres  5887  resieq  5891  dmsnopg  6105  dfco2a  6139  dfpo2  6188  ordeq  6258  limeq  6263  ordunisssuc  6353  iotaeq  6389  sniota  6409  sbcfung  6442  imadif  6502  fneq1  6508  fneq2  6509  feq1  6565  feq2  6566  feq3  6567  sbcfng  6581  sbcfg  6582  f1eq1  6649  f1eq2  6650  f1eq3  6651  foeq1  6668  foeq2  6669  foeq3  6670  f1oeq1  6688  f1oeq2  6689  f1oeq3  6690  mpteqb  6876  rexrnmptw  6953  rexrnmpt  6955  dffo3  6960  fmptco  6983  dff13  7109  f1imaeq  7119  f1imapss  7120  cbvexfo  7142  f1eqcocnv  7153  f1eqcocnvOLD  7154  fliftcnv  7162  isoeq1  7168  isoeq2  7169  isoeq3  7170  isoeq4  7171  isoeq5  7172  isomin  7188  isowe  7200  nfriotadw  7220  mpoeq123  7325  rexrnmpo  7391  iunpw  7599  tfinds  7681  fiun  7759  f1iun  7760  opiota  7872  ottpos  8023  dmtpos  8025  onoviun  8145  smoeq  8152  smoiso2  8171  tfr2b  8198  oarec  8355  oeeui  8395  nnacan  8421  nnmcan  8427  ereq1  8463  ereq2  8464  elecg  8499  ereldm  8504  ixpiin  8670  boxriin  8686  boxcutc  8687  omxpenlem  8813  enfiALT  8934  nnsdomo  8948  isfinite2  9002  ixpfi2  9047  elfi2  9103  fipwss  9118  ennum  9636  cardsdom2  9677  aleph11  9771  alephiso  9785  fin23lem26  10012  compssiso  10061  isf34lem4  10064  isfin5-2  10078  fin1a2lem5  10091  brdom7disj  10218  brdom6disj  10219  fpwwe2lem7  10324  fpwwe2lem11  10328  fpwwe2lem12  10329  genpass  10696  ltasr  10787  axpre-lttri  10852  infm3  11864  creur  11897  eqreznegel  12603  rpneg  12691  ltxr  12780  icoshftf1o  13135  elfzm11  13256  elfzomelpfzo  13419  nn0ennn  13627  nnesq  13870  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  leiso  14101  fz1isolem  14103  pr2pwpr  14121  repsdf2  14419  dfrtrclrec2  14697  rexfiuz  14987  cau4  14996  ello1mpt2  15159  o1lo1  15174  fsumcom2  15414  incexc2  15478  fprodcom2  15622  dvdsflip  15954  bitsmod  16071  bitscmp  16073  smueqlem  16125  divgcdcoprm0  16298  hashdvds  16404  prmreclem2  16546  vdwapun  16603  vdwmc2  16608  imasaddfnlem  17156  comfeq  17332  oppcsect  17407  funcres2b  17528  funcpropd  17532  fullpropd  17552  fthpropd  17553  fthres2b  17562  fthres2c  17563  fullres2c  17571  ffthres2c  17572  fucsect  17606  fucinv  17607  setcsect  17720  pospropd  17960  tosso  18052  odulatb  18067  oduclatb  18140  odudlatb  18158  isipodrs  18170  issgrpv  18292  issgrpn0  18293  mndpropd  18325  mhmpropd  18351  issubm2  18358  efmnd1bas  18447  grppropd  18509  grpinvcnv  18558  conjghm  18780  conjnmzb  18784  ghmpropd  18787  gapm  18827  symg1bas  18913  pmtrfrn  18981  cmnpropd  19311  ablpropd  19312  eqgabl  19351  gsumcom2  19491  dmdprd  19516  dprdw  19528  subgdmdprd  19552  pgpfac1lem2  19593  pgpfac1lem4  19596  ringpropd  19736  crngpropd  19737  crngunit  19819  unitpropd  19854  isnirred  19857  drngpropd  19933  fldpropd  19934  subrgpropd  19974  rhmpropd  19975  acsfn1p  19982  abvpropd  20017  lmodprop2d  20100  lsspropd  20194  lmhmpropd  20250  lbspropd  20276  lvecprop2d  20343  lvecpropd  20344  opprdomn  20485  fiidomfld  20493  phlpropd  20772  assapropd  20986  psrbagconf1o  21049  psrbagconf1oOLD  21050  mplmonmul  21147  ismhp3  21243  mat1dimbas  21529  tpspropd  21995  tgss2  22045  lmbr2  22318  ist1-2  22406  ist1-3  22408  subislly  22540  dissnlocfin  22588  iskgen3  22608  txcnmpt  22683  hausdiag  22704  hauseqlcld  22705  xkococnlem  22718  tgqtop  22771  txhmeo  22862  uffix2  22983  ufildr  22990  txflf  23065  tgphaus  23176  qustgplem  23180  qustgphaus  23182  xpsdsval  23442  blin  23482  blres  23492  xmeterval  23493  xmspropd  23534  mspropd  23535  setsms  23541  metequiv  23571  metustsym  23617  restmetu  23632  ngppropd  23699  xrtgioo  23875  metdsge  23918  icopnfcnv  24011  iccpnfcnv  24013  lmhmclm  24156  lmmbr  24327  equivcmet  24386  cmspropd  24418  iunmbl2  24626  ioombl1lem4  24630  mbfaddlem  24729  i1fmullem  24763  itg1mulc  24774  iblcnlem1  24857  iblrelem  24860  iblre  24863  iblcn  24868  limcun  24964  mvth  25061  ofmulrt  25347  resinf1o  25597  quad2  25894  1cubr  25897  dcubic  25901  wilthlem2  26123  dvdsflf1o  26241  dvdsflsumcom  26242  fsumvma  26266  vmasum  26269  logfac2  26270  logfaclbnd  26275  dchrelbas3  26291  lgsquadlem1  26433  lgsquadlem2  26434  ax5seg  27209  ushgredgedg  27499  ushgredgedgloop  27501  nbumgrvtx  27616  upgriswlk  27910  wspniunwspnon  28189  rusgrnumwwlkb0  28237  isclwwlknx  28301  clwwlknscsh  28327  clwwlknonel  28360  0trl  28387  0spth  28391  0clwlk  28395  0crct  28398  0cycl  28399  eupth2lem2  28484  eucrct2eupth  28510  fusgr2wsp2nb  28599  ocin  29559  chpsscon3  29766  chscllem2  29901  adjval  30153  pjimai  30439  mdsldmd1i  30594  elat2  30603  mdsymi  30674  sbceqbidf  30736  rmoxfrd  30742  rmounid  30744  disjxun0  30814  disjrdx  30831  eqrelrd2  30857  fmptcof2  30896  ofpreima  30904  funcnv5mpt  30907  ressupprn  30926  1stpreima  30941  2ndpreima  30942  fpwrelmapffslem  30969  qsxpid  31460  grplsm0l  31493  smatrcl  31648  locfinreflem  31692  zarcls  31726  zhmnrg  31817  qqhval2  31832  ismntop  31876  reprsuc  32495  reprdifc  32507  bnj919  32647  bnj956  32656  bnj976  32657  bnj1366  32709  bnj916  32813  satfvsucsuc  33227  satfdm  33231  dmopab3rexdif  33267  imaeqsalv  33594  eqfunresadj  33641  ttrclse  33713  xpord3pred  33725  eqscut2  33927  sscoid  34142  dfrdg4  34180  altopthbg  34197  broutsideof3  34355  bj-nnfbi  34834  bj-cbvexdv  34909  bj-sbievw  34958  mobidvALT  34968  bj-restuni  35195  bj-elid6  35268  cbveud  35470  cbvreud  35471  exrecfnlem  35477  wl-ifp-ncond2  35563  wl-ifpimpr  35564  wl-3xorbi123d  35573  wl-sb8eut  35659  wl-sb8mot  35660  wl-clabtv  35675  wl-clabt  35676  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem25  35729  ftc1anclem5  35781  istotbnd3  35856  sstotbnd  35860  heibor  35906  isass  35931  isidlc  36100  smprngopr  36137  brvvdif  36329  elecALTV  36332  eqrel2  36362  dmecd  36367  relcnveq2  36385  elrelscnveq2  36538  extssr  36554  elrefrelsrel  36564  refreleq  36565  elcnvrefrelsrel  36577  elsymrelsrel  36598  symreleq  36599  eltrrelsrel  36622  trreleq  36623  eleqvrelsrel  36634  eqvreleq  36642  redundpim3  36670  erALTVeq1  36708  elfunsALTVfunALTV  36735  eldisjsdisj  36765  eldisjeq  36779  islshpsm  36921  lcvexchlem1  36975  opcon1b  37139  isat3  37248  glbconN  37318  cdleme32fva  38378  cdlemg2cex  38532  dibelval3  39088  dib1dim  39106  doch11  39314  dochsordN  39315  mapdordlem1a  39575  mapd11  39580  mapdsord  39596  mapdcnv11N  39600  mapd0  39606  sn-iotalem  40117  lmhmlvec  40186  fsuppind  40202  mrefg2  40445  jm2.23  40734  wepwsolem  40783  dnwech  40789  islssfg2  40812  gicabl  40840  isdomn3  40945  ifpbi2  40972  ifpbi3  40973  ifpbi23  40978  ifpbi1  40982  ifpbi12  40993  ifpbi13  40994  ontric3g  41027  pwinfig  41057  inintabd  41076  cnvcnvintabd  41097  cnvintabd  41100  intimag  41153  briunov2  41179  heeq12  41273  sbcheg  41276  uneqsn  41522  ntrneineine0lem  41582  ntrneineine1lem  41583  ntrneik2  41591  ntrneix2  41592  ntrneik13  41597  ntrneix13  41598  ralbidar  41952  rexbidar  41953  trsbc  42049  rnmptpr  42602  dffo3f  42606  iccintsng  42951  xlimres  43252  fsetsniunop  44430  fsetsnprcnex  44436  fcoresf1ob  44454  f1cof1b  44456  f1ocof1ob  44460  dfateq12d  44505  aov0nbovbi  44574  fnotaovb  44577  ichbidv  44793  sprsymrelf  44835  prprsprreu  44859  prprreueq  44860  mgmhmpropd  45227  rngcsect  45426  rngcsectALTV  45438  ringcsect  45477  ringcsectALTV  45501  lindslinindsimp2lem5  45691  opndisj  46084  i0oii  46101  io1ii  46102  iscnrm3lem2  46116