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  5818  f1imass  6085  fornex  6655  tposfn2  6876  eroveu  7304  sdomel  7567  ackbij1lem16  8514  ltapr  9324  rpnnen1lem5  11093  qbtwnre  11279  om2uzlt2i  11890  pcpremul  14027  pcaddlem  14067  pockthlem  14083  prmreclem6  14099  catidd  14736  ghmf1  15893  gexdvds  16203  sylow1lem1  16217  lt6abl  16491  ablfacrplem  16687  drnginvrn0  16972  issrngd  17068  islssd  17139  znrrg  18122  isphld  18207  cnllycmp  20659  nmhmcn  20806  minveclem7  21053  ioorcl2  21184  itg2seq  21352  dvlip2  21599  mdegmullem  21681  plyco0  21792  pilem3  22050  sincosq1sgn  22092  sincosq2sgn  22093  logcj  22187  argimgt0  22193  lgseisenlem2  22821  ubthlem2  24423  minvecolem7  24435  nmcexi  25581  lnconi  25588  pjnormssi  25723  tan2h  28571  itg2gt0cn  28594  divrngcl  28910  m1dvdsndvds  30394  lshpcmp  32956  cdlemk35s  34904  cdlemk39s  34906  cdlemk42  34908  dihlspsnat  35301
  Copyright terms: Public domain W3C validator