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

Theorem 3imtr3g 283
 Description: More general version of 3imtr3i 279. 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 232 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4syl6ib 240 1 (𝜑 → (𝜃𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  aleximi  1749  sspwb  4844  ssopab2b  4927  wetrep  5031  imadif  5887  ssoprab2b  6610  suceloni  6905  tfinds2  6955  iiner  7706  fiint  8122  dfac5lem5  8833  axpowndlem3  9300  uzind  11345  isprm5  15257  funcres2  16381  fthres2  16415  ipodrsima  16988  subrgdvds  18617  hausflim  21595  dvres2  23482  axlowdimlem14  25635  atabs2i  28645  esum2dlem  29481  nn0prpw  31488  bj-hbext  31888  heibor1lem  32778  prter2  33184  dvelimf-o  33232  frege70  37247  frege72  37249  frege93  37270  frege110  37287  frege120  37297  pm11.71  37619  sbiota1  37657
 Copyright terms: Public domain W3C validator