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

Theorem 3imtr3g 296
Description: More general version of 3imtr3i 292. 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 244 . 2 (𝜑 → (𝜃𝜒))
4 3imtr3g.3 . 2 (𝜒𝜏)
53, 4syl6ib 252 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  aleximi  1825  sspwb  5337  ssopab2bw  5430  ssopab2b  5432  wetrep  5546  imadif  6434  ssoprab2b  7218  eqoprab2bw  7219  suceloni  7519  tfinds2  7569  iiner  8362  fiint  8787  dfac5lem5  9545  axpowndlem3  10013  uzind  12066  isprm5  16043  funcres2  17160  fthres2  17194  ipodrsima  17767  subrgdvds  19471  hausflim  22507  dvres2  24427  axlowdimlem14  26657  atabs2i  30095  esum2dlem  31239  nn0prpw  33557  bj-hbext  33930  heibor1lem  34957  prter2  35886  dvelimf-o  35934  frege70  40146  frege72  40148  frege93  40169  frege110  40186  frege120  40196  pm11.71  40596  sbiota1  40633
  Copyright terms: Public domain W3C validator