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

Theorem 3imtr3g 298
 Description: More general version of 3imtr3i 294. 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 246 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4syl6ib 254 1 (𝜑 → (𝜃𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  aleximi  1833  sspwb  5307  ssopab2bw  5399  ssopab2b  5401  wetrep  5512  imadif  6408  ssoprab2b  7202  eqoprab2bw  7203  suceloni  7510  tfinds2  7560  iiner  8354  fiint  8781  dfac5lem5  9540  axpowndlem3  10012  uzind  12064  isprm5  16043  funcres2  17162  fthres2  17196  ipodrsima  17769  subrgdvds  19545  hausflim  22593  dvres2  24522  axlowdimlem14  26756  atabs2i  30192  esum2dlem  31473  nn0prpw  33796  bj-hbext  34173  heibor1lem  35263  prter2  36193  dvelimf-o  36241  frege70  40649  frege72  40651  frege93  40672  frege110  40689  frege120  40699  pm11.71  41116  sbiota1  41153
 Copyright terms: Public domain W3C validator