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

Theorem 3imtr3g 284
Description: More general version of 3imtr3i 280. 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 233 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4syl6ib 241 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  aleximi  1908  sspwb  5066  ssopab2b  5152  wetrep  5259  imadif  6134  ssoprab2b  6877  suceloni  7178  tfinds2  7228  iiner  7986  fiint  8402  dfac5lem5  9140  axpowndlem3  9613  uzind  11661  isprm5  15621  funcres2  16759  fthres2  16793  ipodrsima  17366  subrgdvds  18996  hausflim  21986  dvres2  23875  axlowdimlem14  26034  atabs2i  29570  esum2dlem  30463  nn0prpw  32624  bj-hbext  33007  heibor1lem  33921  prter2  34670  dvelimf-o  34718  frege70  38729  frege72  38731  frege93  38752  frege110  38769  frege120  38779  pm11.71  39099  sbiota1  39137
  Copyright terms: Public domain W3C validator