MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr3d Structured version   Unicode version

Theorem 3imtr3d 267
Description: More general version of 3imtr3i 265. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
Hypotheses
Ref Expression
3imtr3d.1  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
3imtr3d.3  |-  ( ph  ->  ( ch  <->  ta )
)
Assertion
Ref Expression
3imtr3d  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr3d
StepHypRef Expression
1 3imtr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
2 3imtr3d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 3imtr3d.3 . . 3  |-  ( ph  ->  ( ch  <->  ta )
)
42, 3sylibd 214 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbird 235 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  tz6.12i  5869  f1imass  6153  fornex  6753  tposfn2  6980  eroveu  7443  sdomel  7702  ackbij1lem16  8647  ltapr  9453  rpnnen1lem5  11257  qbtwnre  11451  om2uzlt2i  12103  m1dvdsndvds  14534  pcpremul  14576  pcaddlem  14616  pockthlem  14632  prmreclem6  14648  catidd  15294  ghmf1  16619  gexdvds  16928  sylow1lem1  16942  lt6abl  17221  ablfacrplem  17436  drnginvrn0  17734  issrngd  17830  islssd  17902  znrrg  18902  isphld  18987  cnllycmp  21748  nmhmcn  21895  minveclem7  22142  ioorcl2  22273  itg2seq  22441  dvlip2  22688  mdegmullem  22770  plyco0  22881  pilem3  23140  sincosq1sgn  23183  sincosq2sgn  23184  logcj  23285  argimgt0  23291  lgseisenlem2  24006  eengtrkg  24705  eengtrkge  24706  ubthlem2  26201  minvecolem7  26213  nmcexi  27358  lnconi  27365  pjnormssi  27500  tan2h  31419  itg2gt0cn  31443  divrngcl  31642  lshpcmp  32006  cdlemk35s  33956  cdlemk39s  33958  cdlemk42  33960  dihlspsnat  34353
  Copyright terms: Public domain W3C validator