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  5705  f1imass  5972  fornex  6541  tposfn2  6762  eroveu  7187  sdomel  7450  ackbij1lem16  8396  ltapr  9206  rpnnen1lem5  10975  qbtwnre  11161  om2uzlt2i  11766  pcpremul  13902  pcaddlem  13942  pockthlem  13958  prmreclem6  13974  catidd  14610  ghmf1  15766  gexdvds  16074  sylow1lem1  16088  lt6abl  16362  ablfacrplem  16554  drnginvrn0  16828  issrngd  16924  islssd  16994  znrrg  17973  isphld  18058  cnllycmp  20503  nmhmcn  20650  minveclem7  20897  ioorcl2  21027  itg2seq  21195  dvlip2  21442  mdegmullem  21524  plyco0  21635  pilem3  21893  sincosq1sgn  21935  sincosq2sgn  21936  logcj  22030  argimgt0  22036  lgseisenlem2  22664  ubthlem2  24223  minvecolem7  24235  nmcexi  25381  lnconi  25388  pjnormssi  25523  tan2h  28377  itg2gt0cn  28400  divrngcl  28716  m1dvdsndvds  30200  lshpcmp  32473  cdlemk35s  34421  cdlemk39s  34423  cdlemk42  34425  dihlspsnat  34818
  Copyright terms: Public domain W3C validator