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

Theorem 3imtr3d 258
Description: More general version of 3imtr3i 256. 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 205 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbird 226 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  tz6.12i  5628  fornex  5833  f1imass  5872  tposfn2  6340  eroveu  6838  sdomel  7093  ltapr  8756  rpnnen1lem5  10435  qbtwnre  10615  om2uzlt2i  11103  pcpremul  12987  pcaddlem  13027  pockthlem  13043  prmreclem6  13059  catidd  13675  ghmf1  14804  gexdvds  14988  sylow1lem1  15002  lt6abl  15274  ablfacrplem  15393  drnginvrn0  15623  issrngd  15719  islssd  15786  znrrg  16619  isphld  16658  cnllycmp  18552  nmhmcn  18699  minveclem7  18897  ioorcl2  19025  itg2seq  19195  dvlip2  19440  mdegmullem  19562  plyco0  19672  pilem3  19930  sincosq1sgn  19967  sincosq2sgn  19968  logcj  20062  argimgt0  20068  lgseisenlem2  20695  ubthlem2  21558  minvecolem7  21570  nmcexi  22714  lnconi  22721  pjnormssi  22856  itg2gt0cn  25495  divrngcl  25911  lshpcmp  29230  cdlemk35s  31178  cdlemk39s  31180  cdlemk42  31182  dihlspsnat  31575
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator