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

Theorem 3imtr3d 270
Description: More general version of 3imtr3i 268. 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 217 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbird 238 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  tz6.12i  5840  f1imass  6119  fornex  6715  tposfn2  6945  eroveu  7408  sdomel  7667  ackbij1lem16  8611  ltapr  9416  rpnnen1lem5  11240  qbtwnre  11438  om2uzlt2i  12110  m1dvdsndvds  14687  pcpremul  14731  pcaddlem  14771  pockthlem  14787  prmreclem6  14803  catidd  15524  ghmf1  16849  gexdvds  17173  sylow1lem1  17188  lt6abl  17467  ablfacrplem  17636  drnginvrn0  17931  issrngd  18027  islssd  18097  znrrg  19073  isphld  19158  cnllycmp  21921  nmhmcn  22071  minveclem7  22314  minveclem7OLD  22326  ioorcl2  22461  itg2seq  22637  dvlip2  22884  mdegmullem  22964  plyco0  23083  pilem3  23346  pilem3OLD  23347  sincosq1sgn  23390  sincosq2sgn  23391  logcj  23492  argimgt0  23498  lgseisenlem2  24215  eengtrkg  24952  eengtrkge  24953  ubthlem2  26450  minvecolem7  26462  minvecolem7OLD  26472  nmcexi  27616  lnconi  27623  pjnormssi  27758  tan2h  31844  itg2gt0cn  31904  divrngcl  32103  lshpcmp  32466  cdlemk35s  34416  cdlemk39s  34418  cdlemk42  34420  dihlspsnat  34813  clcnvlem  36143
  Copyright terms: Public domain W3C validator