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

Theorem 3imtr3g 295
Description: More general version of 3imtr3i 291. 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, 2biimtrrid 242 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4syl6ib 251 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  aleximi  1835  rexim  3087  sspwb  5410  ssopab2bw  5508  ssopab2b  5510  wetrep  5630  imadif  6589  ssoprab2b  7430  eqoprab2bw  7431  sucexeloniOLD  7749  suceloniOLD  7751  tfinds2  7804  iiner  8734  fsetcdmex  8807  fiint  9274  dfac5lem5  10071  axpowndlem3  10543  uzind  12603  isprm5  16591  funcres2  17792  fthres2  17827  ipodrsima  18438  subrgdvds  20278  hausflim  23355  dvres2  25299  axlowdimlem14  27953  atabs2i  31393  esum2dlem  32755  nn0prpw  34848  bj-hbext  35228  heibor1lem  36318  prter2  37393  dvelimf-o  37441  frege70  42297  frege72  42299  frege93  42320  frege110  42337  frege120  42347  pm11.71  42769  sbiota1  42806
  Copyright terms: Public domain W3C validator