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

Theorem 3bitr3g 300
Description: More general version of 3bitr3i 288. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
Hypotheses
Ref Expression
3bitr3g.1 (𝜑 → (𝜓𝜒))
3bitr3g.2 (𝜓𝜃)
3bitr3g.3 (𝜒𝜏)
Assertion
Ref Expression
3bitr3g (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr3g
StepHypRef Expression
1 3bitr3g.2 . . 3 (𝜓𝜃)
2 3bitr3g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5bbr 272 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4syl6bb 274 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  notbid  306  cador  1537  equequ2OLD  1905  cbvexdva  2174  dfsbcq2  3309  unineq  3739  iindif2  4423  reusv2  4699  rabxfrd  4714  opeqex  4785  eqbrrdv  5033  eqbrrdiv  5034  opelco2g  5103  opelcnvg  5116  ralrnmpt  6165  fliftcnv  6343  eusvobj2  6424  ottpos  7129  smoiso  7226  ercnv  7530  ordiso2  8183  cantnfrescl  8336  cantnfp1lem3  8340  cantnflem1b  8346  cantnflem1  8349  cnfcom  8360  cnfcom3lem  8363  carden2  8576  cardeq0  9133  axpownd  9182  fpwwe2lem9  9219  fzen  12101  hasheq0  12884  incexc2  14282  divalglem4  14831  divalglem8  14836  divalgb  14841  divalgmodOLD  14844  sadadd  14904  sadass  14908  smuval2  14919  smumul  14930  isprm3  15114  vdwmc  15408  imasleval  15920  acsfn2  16043  invsym2  16142  yoniso  16644  pmtrfmvdn0  17601  dprd2d2  18177  cmpfi  20928  xkoinjcn  21207  tgpconcomp  21633  iscau3  22752  mbfimaopnlem  23107  ellimc3  23328  eldv  23347  eltayl  23809  atandm3  24296  el2wlkonot  26138  el2spthonot  26139  rmoxfrdOLD  28508  rmoxfrd  28509  opeldifid  28586  2ndpreima  28660  f1od2  28679  ordtconlem1  29098  bnj1253  30188  wl-dral1d  32390  wl-sb8et  32407  wl-equsb3  32410  wl-sb8eut  32432  wl-ax11-lem8  32442  poimirlem2  32475  poimirlem16  32489  poimirlem18  32491  poimirlem21  32494  poimirlem22  32495  eqbrrdv2  33060  islpln5  33733  islvol5  33777  ntrneicls11  37309  radcnvrat  37436  trsbc  37672  aacllem  42426
  Copyright terms: Public domain W3C validator