MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr4g Structured version   Visualization version   GIF version

Theorem 3bitr4g 315
Description: More general version of 3bitr4i 304. 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
StepHypRef Expression
1 3bitr4g.2 . . 3 (𝜃𝜓)
2 3bitr4g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5bb 284 . 2 (𝜑 → (𝜃𝜒))
4 3bitr4g.3 . 2 (𝜏𝜒)
53, 4syl6bbr 290 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  bibi1d  345  pm5.32rd  578  orbi2d  909  orbi1d  910  ifpbi123d  1069  3orbi123d  1426  3anbi123d  1427  nanbi1  1485  nanbi2  1486  xorbi12d  1509  hadbi123d  1586  had0  1596  cadbi123d  1602  nfbiit  1842  nfbidv  1914  sbequ  2081  nfbidf  2217  drex1v  2381  drnf1v  2382  drex1  2458  drnf1  2460  sb4b  2495  sb4bOLD  2496  drsb1  2531  eujustALT  2653  eubi  2665  eleq1ab  2801  eqeq1d  2823  eqeq1dALT  2824  eqeq2d  2832  abbi1  2884  eleq1w  2895  eleq2w  2896  eleq1d  2897  eleq2d  2898  eleq2dALT  2899  abbi2dv  2950  nfceqdf  2972  drnfc1  2997  drnfc1OLD  2998  drnfc2  2999  neleq12d  3127  ralbidv2  3195  r19.21t  3214  ralbida  3230  rexbidv2  3295  r19.23t  3313  rexbida  3318  ralrexbid  3322  ralcom2w  3363  ralcom2  3364  reubida  3388  reubidva  3389  rmobida  3393  raleqf  3398  rexeqf  3399  reueq1f  3400  rmoeq1f  3401  reueq1  3408  rmoeq1  3409  cbvraldva2  3457  cbvrexdva2  3458  cbvrexdva2OLD  3459  dfsbcq  3773  sbceqbid  3778  sbcbid  3825  sbcbi2OLD  3831  eqsbc3r  3836  sbcrext  3855  sbcabel  3860  psseq1  4063  psseq2  4064  ssconb  4113  uneq1  4131  ineq1OLD  4181  difin2  4265  reuun2  4285  sbcnel12g  4362  sbnfc2  4387  reldisj  4400  undif4  4414  disjssun  4415  pssdifcom1  4433  pssdifcom2  4434  sbcssg  4461  eltpg  4617  raltpg  4628  rextpg  4629  r19.12sn  4650  intmin4  4898  dfiun2g  4947  dfiun2gOLD  4948  iindif1  4989  iindif2  4991  iinin2  4992  disjprgw  5053  disjprg  5054  disjxun  5056  breq  5060  breq1  5061  breq2  5062  treq  5170  reusv2lem5  5294  rexxfrd  5301  rexxfr2d  5303  rexxfrd2  5305  rabxfrd  5309  opthg2  5363  oteqex2  5381  oteqex  5382  poeq1  5471  soeq1  5488  freq1  5519  weeq1  5537  weeq2  5538  opthprc  5610  wesn  5634  releq  5645  sbcrel  5649  eqrel  5652  eqrelrel  5664  xpiindi  5700  dmopab2rex  5780  dfres3  5852  brres  5854  resieq  5858  dmsnopg  6064  dfco2a  6093  ordeq  6192  limeq  6197  ordunisssuc  6287  iotaeq  6320  sniota  6340  sbcfung  6373  imadif  6432  fneq1  6438  fneq2  6439  feq1  6489  feq2  6490  feq3  6491  sbcfng  6505  sbcfg  6506  f1eq1  6564  f1eq2  6565  f1eq3  6566  foeq1  6580  foeq2  6581  foeq3  6582  f1oeq1  6598  f1oeq2  6599  f1oeq3  6600  mpteqb  6780  rexrnmptw  6854  rexrnmpt  6856  dffo3  6861  fmptco  6884  dff13  7004  f1imaeq  7014  f1imapss  7015  cbvexfo  7037  f1eqcocnv  7048  fliftcnv  7053  isoeq1  7059  isoeq2  7060  isoeq3  7061  isoeq4  7062  isoeq5  7063  isomin  7079  isowe  7091  nfriotadw  7111  mpoeq123  7215  rexrnmpo  7279  iunpw  7481  tfinds  7562  fiunw  7632  f1iunw  7633  fiun  7635  f1iun  7636  opiota  7748  ottpos  7893  dmtpos  7895  onoviun  7971  smoeq  7978  smoiso2  7997  tfr2b  8023  oarec  8178  oeeui  8218  nnacan  8244  nnmcan  8250  ereq1  8286  ereq2  8287  elecg  8322  ereldm  8327  ixpiin  8477  boxriin  8493  boxcutc  8494  omxpenlem  8607  nnsdomo  8702  enfi  8723  isfinite2  8765  ixpfi2  8811  elfi2  8867  fipwss  8882  ennum  9365  cardsdom2  9406  aleph11  9499  alephiso  9513  fin23lem26  9736  compssiso  9785  isf34lem4  9788  isfin5-2  9802  fin1a2lem5  9815  brdom7disj  9942  brdom6disj  9943  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  genpass  10420  ltasr  10511  axpre-lttri  10576  infm3  11589  creur  11621  eqreznegel  12323  rpneg  12411  ltxr  12500  icoshftf1o  12850  elfzm11  12968  elfzomelpfzo  13131  nn0ennn  13337  nnesq  13578  hashbclem  13800  hashf1lem1  13803  leiso  13807  fz1isolem  13809  pr2pwpr  13827  repsdf2  14130  dfrtrclrec2  14406  rexfiuz  14697  cau4  14706  ello1mpt2  14869  o1lo1  14884  fsumcom2  15119  incexc2  15183  fprodcom2  15328  dvdsflip  15657  bitsmod  15775  bitscmp  15777  smueqlem  15829  divgcdcoprm0  15999  hashdvds  16102  prmreclem2  16243  vdwapun  16300  vdwmc2  16305  imasaddfnlem  16791  comfeq  16966  oppcsect  17038  funcres2b  17157  funcpropd  17160  fullpropd  17180  fthpropd  17181  fthres2b  17190  fthres2c  17191  fullres2c  17199  ffthres2c  17200  fucsect  17232  fucinv  17233  setcsect  17339  tosso  17636  pospropd  17734  odulatb  17743  oduclatb  17744  isipodrs  17761  odudlatb  17796  issgrpv  17893  issgrpn0  17894  mndpropd  17926  mhmpropd  17952  issubm2  17959  grppropd  18058  grpinvcnv  18107  conjghm  18329  conjnmzb  18333  ghmpropd  18336  gapm  18376  symg1bas  18455  pmtrfrn  18517  cmnpropd  18847  ablpropd  18848  eqgabl  18886  gsumcom2  19026  dmdprd  19051  dprdw  19063  subgdmdprd  19087  pgpfac1lem2  19128  pgpfac1lem4  19131  ringpropd  19263  crngpropd  19264  crngunit  19343  unitpropd  19378  isnirred  19381  drngpropd  19460  fldpropd  19461  subrgpropd  19501  rhmpropd  19502  acsfn1p  19509  abvpropd  19544  lmodprop2d  19627  lsspropd  19720  lmhmpropd  19776  lbspropd  19802  lvecprop2d  19869  lvecpropd  19870  opprdomn  20004  fiidomfld  20011  assapropd  20031  psrbagconf1o  20084  mplmonmul  20175  phlpropd  20729  mat1dimbas  21011  tpspropd  21476  tgss2  21525  lmbr2  21797  ist1-2  21885  ist1-3  21887  subislly  22019  dissnlocfin  22067  iskgen3  22087  txcnmpt  22162  hausdiag  22183  hauseqlcld  22184  xkococnlem  22197  tgqtop  22250  txhmeo  22341  uffix2  22462  ufildr  22469  txflf  22544  tgphaus  22654  qustgplem  22658  qustgphaus  22660  xpsdsval  22920  blin  22960  blres  22970  xmeterval  22971  xmspropd  23012  mspropd  23013  setsms  23019  metequiv  23048  metustsym  23094  restmetu  23109  ngppropd  23175  xrtgioo  23343  metdsge  23386  icopnfcnv  23475  iccpnfcnv  23477  lmhmclm  23620  lmmbr  23790  equivcmet  23849  cmspropd  23881  iunmbl2  24087  ioombl1lem4  24091  mbfaddlem  24190  i1fmullem  24224  itg1mulc  24234  iblcnlem1  24317  iblrelem  24320  iblre  24323  iblcn  24328  limcun  24422  mvth  24518  ofmulrt  24800  resinf1o  25047  quad2  25344  1cubr  25347  dcubic  25351  wilthlem2  25574  dvdsflf1o  25692  dvdsflsumcom  25693  fsumvma  25717  vmasum  25720  logfac2  25721  logfaclbnd  25726  dchrelbas3  25742  lgsquadlem1  25884  lgsquadlem2  25885  ax5seg  26652  ushgredgedg  26939  ushgredgedgloop  26941  nbumgrvtx  27056  upgriswlk  27350  wspniunwspnon  27630  rusgrnumwwlkb0  27678  isclwwlknx  27742  clwwlknscsh  27769  clwwlknonel  27802  0trl  27829  0spth  27833  0clwlk  27837  0crct  27840  0cycl  27841  eupth2lem2  27926  eucrct2eupth  27952  fusgr2wsp2nb  28041  ocin  29001  chpsscon3  29208  chscllem2  29343  adjval  29595  pjimai  29881  mdsldmd1i  30036  elat2  30045  mdsymi  30116  sbceqbidf  30178  rmoxfrd  30185  rmounid  30187  disjxun0  30253  disjrdx  30270  eqrelrd2  30296  fmptcof2  30331  ofpreima  30339  funcnv5mpt  30342  1stpreima  30369  2ndpreima  30370  fpwrelmapffslem  30395  qsxpid  30855  smatrcl  30961  locfinreflem  31004  zhmnrg  31108  qqhval2  31123  ismntop  31167  reprsuc  31786  reprdifc  31798  bnj919  31938  bnj956  31948  bnj976  31949  bnj1366  32001  bnj916  32105  satfvsucsuc  32510  satfdm  32514  dmopab3rexdif  32550  dfpo2  32889  eqfunresadj  32902  sscoid  33272  dfrdg4  33310  altopthbg  33327  broutsideof3  33485  bj-nnfbi  33955  bj-cbvexdv  34020  bj-sbievw  34069  mobidvALT  34079  bj-restuni  34283  bj-elid6  34355  cbveud  34536  cbvreud  34537  exrecfnlem  34543  wl-sb8eut  34695  wl-sb8mot  34696  wl-clabtv  34711  wl-clabt  34712  wl-dfralf  34721  wl-dfrexf  34729  wl-dfrmof  34737  wl-dfreuf  34741  wl-dfrabf  34746  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem25  34799  ftc1anclem5  34853  istotbnd3  34932  sstotbnd  34936  heibor  34982  isass  35007  isidlc  35176  smprngopr  35213  brvvdif  35407  elecALTV  35410  eqrel2  35440  dmecd  35445  relcnveq2  35463  elrelscnveq2  35615  extssr  35631  elrefrelsrel  35641  refreleq  35642  elcnvrefrelsrel  35654  elsymrelsrel  35675  symreleq  35676  eltrrelsrel  35699  trreleq  35700  eleqvrelsrel  35711  eqvreleq  35719  redundpim3  35747  erALTVeq1  35785  elfunsALTVfunALTV  35812  eldisjsdisj  35842  eldisjeq  35856  islshpsm  35998  lcvexchlem1  36052  opcon1b  36216  isat3  36325  glbconN  36395  cdleme32fva  37455  cdlemg2cex  37609  dibelval3  38165  dib1dim  38183  doch11  38391  dochsordN  38392  mapdordlem1a  38652  mapd11  38657  mapdsord  38673  mapdcnv11N  38677  mapd0  38683  lmhmlvec  39028  mrefg2  39184  jm2.23  39473  wepwsolem  39522  dnwech  39528  islssfg2  39551  gicabl  39579  isdomn3  39684  ifpbi2  39712  ifpbi3  39713  ifpbi23  39718  ifpbi1  39723  ifpbi12  39734  ifpbi13  39735  ontric3g  39768  pwinfig  39800  inintabd  39819  cnvcnvintabd  39840  cnvintabd  39843  intimag  39881  briunov2  39907  heeq12  40002  sbcheg  40005  rcompleq  40250  uneqsn  40253  ntrneineine0lem  40313  ntrneineine1lem  40314  ntrneik2  40322  ntrneix2  40323  ntrneik13  40328  ntrneix13  40329  ralbidar  40657  rexbidar  40658  trsbc  40754  rnmptpr  41313  dffo3f  41318  iccintsng  41679  xlimres  41982  dfateq12d  43206  aov0nbovbi  43275  fnotaovb  43278  sprsymrelf  43504  prprsprreu  43528  prprreueq  43529  mgmhmpropd  43899  efmnd1bas  43960  rngcsect  44149  rngcsectALTV  44161  ringcsect  44200  ringcsectALTV  44224  lindslinindsimp2lem5  44415
  Copyright terms: Public domain W3C validator