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

Theorem 3imtr3g 295
Description: More general version of 3imtr3i 291. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypotheses
Ref Expression
3imtr3g.1 (𝜑 → (𝜓𝜒))
3imtr3g.2 (𝜓𝜃)
3imtr3g.3 (𝜒𝜏)
Assertion
Ref Expression
3imtr3g (𝜑 → (𝜃𝜏))

Proof of Theorem 3imtr3g
StepHypRef Expression
1 3imtr3g.2 . . 3 (𝜓𝜃)
2 3imtr3g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2biimtrrid 243 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4imbitrdi 251 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  aleximi  1832  rexim  3087  sspwb  5454  ssopab2bw  5552  ssopab2b  5554  wetrep  5678  imadif  6650  ssoprab2b  7502  eqoprab2bw  7503  sucexeloniOLD  7830  suceloniOLD  7832  tfinds2  7885  iiner  8829  fsetcdmex  8903  fiint  9366  fiintOLD  9367  dfac5lem5  10167  axpowndlem3  10639  uzind  12710  isprm5  16744  funcres2  17943  fthres2  17979  ipodrsima  18586  subrgdvds  20586  hausflim  23989  dvres2  25947  precsexlem11  28241  uzsind  28391  axlowdimlem14  28970  atabs2i  32421  esum2dlem  34093  nn0prpw  36324  bj-hbext  36711  heibor1lem  37816  prter2  38882  dvelimf-o  38930  frege70  43946  frege72  43948  frege93  43969  frege110  43986  frege120  43996  pm11.71  44416  sbiota1  44453
  Copyright terms: Public domain W3C validator