Theorem 3bitr4g 317

Description: More general version of 3bitr4i 306. 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	bitrid 286	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 292	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  pm5.32rd  589  orbi2d  929  orbi1d  930  ifpbi123d  1095  3orbi123d  1463  3anbi123d  1464  nanbi1  1531  nanbi2  1532  xorbi12d  1555  hadbi123d  1625  had0OLD  1636  cadbi123d  1643  nfbiit  1884  nfbidv  1955  sbequ  2120  nfbidf  2261  drex1v  2400  drnf1v  2401  drex1  2471  drnf1  2473  sb4b  2505  drsb1  2525  eujustALT  2598  eubi  2610  eleq1ab  2741  eqeq1d  2763  eqeq1dALT  2764  eqeq2d  2772  abbi  2826  eleq1w  2844  eleq2w  2845  eleq1d  2846  eleq2d  2847  eleq2dALT  2848  eqabdv  2894  nfceqdf  2919  drnfc1  2942  drnfc2  2943  neleq12d  3067  ralbidv2  3182  rexbidv2  3183  r19.21t  3257  r19.23t  3259  rexbida  3275  rexeq  3316  cbvraldva2  3337  raleqf  3342  ralcom2  3363  rmobidva  3379  reubidva  3380  rmobida  3389  reubida  3390  rmoeq1  3397  reueq1  3398  reueqbidv  3402  rmoeq1f  3403  reueq1f  3404  dfsbcq  3741  sbceqbid  3746  sbcbid  3793  sbcbi2  3797  eqsbc2  3802  sbcrext  3820  sbcabel  3825  ralss  4004  rexss  4005  psseq1  4038  psseq2  4039  ssconb  4089  uneq1  4108  difin2  4247  rcompleq  4251  reuun2  4271  sbcnel12g  4372  sbnfc2  4397  reldisj  4406  undif4  4420  disjssun  4421  pssdifcom1  4445  pssdifcom2  4446  sbcssg  4477  eltpg  4647  raltpg  4659  rextpg  4660  r19.12sn  4681  intmin4  4937  dfiun2g  4988  iindif1  5035  iindif2  5037  iinin2  5038  disjprg  5099  disjxun  5101  breq  5105  breq1  5106  breq2  5107  treq  5219  reusv2lem5  5364  rexxfrd  5371  rexxfr2d  5373  rexxfrd2  5375  rabxfrd  5379  opthg2  5448  oteqex2  5471  oteqex  5472  poeq1  5562  soeq1  5580  freq1  5618  weeq1  5638  weeq2  5639  opthprc  5715  wesn  5740  releq  5753  sbcrel  5757  eqrel  5760  eqrelrel  5773  xpiindi  5812  dmopab2rex  5899  dfres3  5975  brres  5977  resieq  5981  dmsnopg  6214  dfco2a  6247  dfpo2  6299  ordeq  6369  limeq  6374  ordunisssuc  6471  iotaeq  6506  sniota  6529  sbcfung  6563  sbcfungOLD  6564  imadif  6624  fneq1  6630  fneq2  6631  feq1  6687  feq2  6688  feq3  6689  sbcfng  6706  sbcfg  6707  f1eq1  6773  f1eq2  6774  f1eq3  6775  foeq1  6792  foeq2  6793  foeq3  6794  f1oeq1  6812  f1oeq2  6813  f1oeq3  6814  mpteqb  7013  rexrnmptw  7095  rexrnmpt  7097  dffo3  7102  dffo3f  7106  fmptco  7130  rexima  7244  dff13  7258  f1imaeq  7269  f1imapss  7270  cbvexfo  7298  f1eqcocnv  7309  fliftcnv  7319  isoeq1  7325  isoeq2  7326  isoeq3  7327  isoeq4  7328  isoeq5  7329  isomin  7345  isowe  7357  eqfunresadj  7370  nfriotadw  7385  mpoeq123  7492  rexrnmpo  7560  iunpw  7785  tfinds  7871  resf1extb  7946  fiun  7955  f1iun  7956  opiota  8070  xpord3pred  8169  ottpos  8253  dmtpos  8255  onoviun  8351  smoeq  8358  smoiso2  8377  tfr2b  8404  oarec  8570  oeeui  8611  nnacan  8637  nnmcan  8643  ereq1  8725  ereq2  8726  elecg  8762  ereldm  8771  ixpiin  8952  boxriin  8968  boxcutc  8969  omxpenlem  9097  enfiALT  9203  nnsdomo  9234  isfinite2  9290  ixpfi2  9339  elfi2  9406  fipwss  9421  ttrclse  9728  ennum  10028  cardsdom2  10069  aleph11  10163  alephiso  10177  fin23lem26  10403  compssiso  10452  isf34lem4  10455  isfin5-2  10469  fin1a2lem5  10482  brdom7disj  10610  brdom6disj  10611  fpwwe2lem7  10722  fpwwe2lem11  10726  fpwwe2lem12  10727  genpass  11094  ltasr  11185  axpre-lttri  11250  infm3  12276  creur  12314  eqreznegel  13061  rpneg  13154  ltxr  13244  icoshftf1o  13605  elfzm11  13729  elfzomelpfzo  13907  nn0ennn  14122  nnesq  14371  hashbclem  14597  hashf1lem1  14600  leiso  14604  fz1isolem  14606  pr2pwpr  14624  repsdf2  14929  dfrtrclrec2  15211  rexfiuz  15515  cau4  15524  ello1mpt2  15689  o1lo1  15704  fsumcom2  15940  incexc2  16007  fprodcom2  16151  dvdsflip  16487  bitsmod  16606  bitscmp  16608  smueqlem  16660  divgcdcoprm0  16840  hashdvds  16952  prmreclem2  17095  vdwapun  17152  vdwmc2  17157  imasaddfnlem  17700  comfeq  17880  oppcsect  17953  funcres2b  18072  funcpropd  18077  fullpropd  18097  fthpropd  18098  fthres2b  18107  fthres2c  18108  fullres2c  18116  ffthres2c  18117  fucsect  18150  fucinv  18151  setcsect  18264  pospropd  18499  tosso  18591  odulatb  18608  oduclatb  18681  odudlatb  18699  isipodrs  18711  mgmhmpropd  18887  issgrpv  18910  issgrpn0  18911  mndpropd  18951  mhmpropd  18987  issubm2  18999  efmnd1bas  19089  grppropd  19162  grpinvcnv  19217  qsxpid  19387  conjghm  19463  conjnmzb  19467  ghmpropd  19470  gapm  19520  symg1bas  19605  pmtrfrn  19672  cmnpropd  20005  ablpropd  20006  eqgabl  20048  gsumcom2  20189  dmdprd  20214  dprdw  20226  subgdmdprd  20250  pgpfac1lem2  20291  pgpfac1lem4  20294  rngpropd  20396  ringpropd  20519  crngpropd  20520  crngunit  20608  unitpropd  20647  isnirred  20650  nzrpropd  20771  issubrng  20799  subrngpropd  20820  resrhm2b  20854  subrgpropd  20860  rhmpropd  20861  rngcsect  20888  ringcsect  20922  isdomn3  20966  drngpropd  21027  fldpropd  21028  fiidomfld  21032  acsfn1p  21056  abvpropd  21092  lmodprop2d  21199  lsspropd  21292  lmhmpropd  21348  lbspropd  21374  lmhmlvec  21385  lvecprop2d  21444  lvecpropd  21445  df2idl2rng  21550  pzriprnglem10  21796  phlpropd  21961  assapropd  22179  psrbagconf1o  22237  mplmonmul  22345  ismhp3  22463  mat1dimbas  22787  tpspropd  23256  tgss2  23305  lmbr2  23577  ist1-2  23665  ist1-3  23667  subislly  23800  dissnlocfin  23848  iskgen3  23868  txcnmpt  23943  hausdiag  23964  hauseqlcld  23965  xkococnlem  23978  tgqtop  24031  txhmeo  24122  uffix2  24243  ufildr  24250  txflf  24325  tgphaus  24436  qustgplem  24440  qustgphaus  24442  xpsdsval  24700  blin  24740  blres  24750  xmeterval  24751  xmspropd  24792  mspropd  24793  setsms  24799  metequiv  24828  metustsym  24874  restmetu  24889  ngppropd  24956  xrtgioo  25126  metdsge  25169  icopnfcnv  25263  iccpnfcnv  25265  lmhmclm  25408  lmmbr  25579  equivcmet  25638  cmspropd  25670  iunmbl2  25878  ioombl1lem4  25882  mbfaddlem  25981  i1fmullem  26015  itg1mulc  26025  iblcnlem1  26108  iblrelem  26111  iblre  26114  iblcn  26119  limcun  26215  mvth  26312  ofmulrt  26600  resinf1o  26864  quad2  27167  1cubr  27170  dcubic  27174  wilthlem2  27396  dvdsflf1o  27514  dvdsflsumcom  27515  fsumvma  27540  vmasum  27543  logfac2  27544  logfaclbnd  27549  dchrelbas3  27565  lgsquadlem1  27707  lgsquadlem2  27708  eqcuts2  28172  mulsrid  28499  z12sge0  28869  readdscl  28885  elplng  29258  plngcplem  29263  ax5seg  29516  ushgredgedg  29810  ushgredgedgloop  29812  nbumgrvtx  29927  upgriswlk  30221  wspniunwspnon  30512  rusgrnumwwlkb0  30563  isclwwlknx  30627  clwwlknscsh  30653  clwwlknonel  30686  0trl  30713  0spth  30717  0clwlk  30721  0crct  30724  0cycl  30725  eupth2lem2  30820  eucrct2eupth  30846  fusgr2wsp2nb  30935  ocin  31898  chpsscon3  32105  chscllem2  32240  adjval  32492  pjimai  32778  mdsldmd1i  32933  elat2  32942  mdsymi  33013  sbceqbidf  33083  rmoxfrd  33089  rmounid  33091  disjxun0  33168  disjrdx  33185  eqrelrd2  33210  fmptcof2  33251  ofpreima  33259  funcnv5mpt  33261  ressupprn  33283  1stpreima  33300  2ndpreima  33301  fpwrelmapffslem  33324  cntrval2  33732  domnpropd  33841  idompropd  33842  subsdrg  33860  grplsm0l  33954  opprlidlabs  34009  ressply1mon1p  34100  psrmonmul  34182  algextdeglem6  34354  smatrcl  34428  locfinreflem  34472  zarcls  34506  zhmnrg  34597  qqhval2  34614  ismntop  34658  reprsuc  35244  reprdifc  35256  bnj919  35398  bnj956  35407  bnj976  35408  bnj1366  35459  bnj916  35563  satfvsucsuc  36130  satfdm  36134  dmopab3rexdif  36170  rexxfr3dALT  36404  sscoid  36675  dfrdg4  36715  altopthbg  36733  broutsideof3  36891  rmoeqbidv  37002  sbequbidv  37003  disjeq12dv  37004  ixpeq12dv  37005  cbvmodavw  37039  cbveudavw  37040  cbvrmodavw  37041  cbvreudavw  37042  cbvsbdavw  37043  cbvsbdavw2  37044  cbvabdavw  37045  cbvsbcdavw  37046  cbvsbcdavw2  37047  cbvdisjdavw  37057  cbvrmodavw2  37072  cbvreudavw2  37073  cbvdisjdavw2  37078  bj-nnfbi  37649  bj-cbvexdv  37712  bj-sbievw  37759  mobidvALT  37769  bj-axreprepsep  37991  bj-restuni  38018  bj-elid6  38091  cbveud  38295  cbvreud  38296  exrecfnlem  38302  wl-ifp-ncond2  38388  wl-ifpimpr  38389  wl-3xorbi123d  38398  wl-sb8eut  38510  wl-sb8eutv  38511  wl-sb8mot  38512  wl-sb8motv  38513  wl-clabtv  38518  wl-clabt  38519  wl-eujustlem1  38520  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem25  38563  ftc1anclem5  38615  istotbnd3  38705  sstotbnd  38709  heibor  38755  isass  38780  isidlc  38949  smprngopr  38986  brvvdif  39200  elecALTV  39203  eqrel2  39237  dmecd  39242  relcnveq2  39261  eldmxrncnvepres  39366  eldmxrncnvepres2  39367  extssr  39521  elrefrelsrel  39532  refreleq  39533  elcnvrefrelsrel  39548  elrelscnveq2  39561  elsymrelsrel  39573  symreleq  39574  eltrrelsrel  39597  trreleq  39598  eleqvrelsrel  39610  eqvreleq  39618  redundpim3  39646  erALTVeq1  39686  elfunsALTVfunALTV  39714  eldisjsdisj  39756  eldisjeq  39773  disjsuc  39791  parteq1  39809  parteq2  39810  islshpsm  40037  lcvexchlem1  40091  opcon1b  40255  isat3  40364  glbconN  40434  cdleme32fva  41494  cdlemg2cex  41648  dibelval3  42204  dib1dim  42222  doch11  42430  dochsordN  42431  mapdordlem1a  42691  mapd11  42696  mapdsord  42712  mapdcnv11N  42716  mapd0  42722  sn-iotalem  43275  ricfld  43594  fimgmcyc  43598  fsuppind  43618  mrefg2  43717  jm2.23  44002  wepwsolem  44048  dnwech  44054  islssfg2  44072  gicabl  44100  onsupmaxb  44240  onsupeqnmax  44248  orddif0suc  44269  oadif1lem  44380  oadif1  44381  fzunt  44455  fzuntd  44456  fzunt1d  44457  fzuntgd  44458  ifpbi2  44467  ifpbi3  44468  ifpbi1  44477  ifpbi12  44488  ifpbi13  44489  ontric3g  44522  pwinfig  44561  inintabd  44579  cnvcnvintabd  44599  cnvintabd  44602  intimag  44655  briunov2  44681  heeq12  44775  sbcheg  44778  uneqsn  45024  ntrneineine0lem  45082  ntrneineine1lem  45083  ntrneik2  45091  ntrneix2  45092  ntrneik13  45097  ntrneix13  45098  ralbidar  45427  rexbidar  45428  trsbc  45522  cocan2g  45922  cocan1g  45924  relpeq1  45933  relpeq2  45934  relpeq3  45935  relpeq4  45936  relpeq5  45937  n0abso  45965  modelaxreplem3  45969  iindif2f  46174  rnmptpr  46191  iccintsng  46534  xlimres  46830  fsetsniunop  48118  fsetsnprcnex  48124  fcoresf1ob  48142  f1cof1b  48146  f1ocof1ob  48150  dfateq12d  48195  aov0nbovbi  48264  fnotaovb  48267  ichbidv  48534  sprsymrelf  48576  prprsprreu  48600  prprreueq  48601  nprmmul1  48608  edgusgrclnbfin  48939  dfclnbgr6  48953  dfnbgr6  48954  isubgredg  48963  gpgnbgrvtx0  49171  gpgnbgrvtx1  49172  rngcsectALTV  49371  ringcsectALTV  49405  lindslinindsimp2lem5  49573  xpco2  49966  opndisj  50010  i0oii  50027  io1ii  50028  iscnrm3lem2  50042  uobffth  50325  uobeqw  50326  thincpropd  50549  termcpropd  50610  alsbid  50897