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  1799  sspwb  4947  ssopab2b  5031  wetrep  5136  imadif  6011  ssoprab2b  6754  suceloni  7055  tfinds2  7105  iiner  7862  fiint  8278  dfac5lem5  8988  axpowndlem3  9459  uzind  11507  isprm5  15466  funcres2  16605  fthres2  16639  ipodrsima  17212  subrgdvds  18842  hausflim  21832  dvres2  23721  axlowdimlem14  25880  atabs2i  29389  esum2dlem  30282  nn0prpw  32443  bj-hbext  32826  heibor1lem  33738  prter2  34485  dvelimf-o  34533  frege70  38544  frege72  38546  frege93  38567  frege110  38584  frege120  38594  pm11.71  38914  sbiota1  38952
  Copyright terms: Public domain W3C validator