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

Theorem 3imtr3g 287
Description: More general version of 3imtr3i 283. 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, 2syl5bir 235 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4syl6ib 243 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  aleximi  1927  sspwb  5108  ssopab2b  5198  wetrep  5305  imadif  6184  ssoprab2b  6946  suceloni  7247  tfinds2  7297  iiner  8057  fiint  8479  dfac5lem5  9236  axpowndlem3  9709  uzind  11759  isprm5  15752  funcres2  16872  fthres2  16906  ipodrsima  17480  subrgdvds  19112  hausflim  22113  dvres2  24017  axlowdimlem14  26192  atabs2i  29786  esum2dlem  30670  nn0prpw  32830  bj-hbext  33206  heibor1lem  34095  prter2  34902  dvelimf-o  34950  frege70  39009  frege72  39011  frege93  39032  frege110  39049  frege120  39059  pm11.71  39379  sbiota1  39416
  Copyright terms: Public domain W3C validator