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

Theorem 3imtr3d 275
Description: More general version of 3imtr3i 273. 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 222 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbird 243 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  tz6.12i  5908  f1imass  6190  fornex  6789  tposfn2  7021  eroveu  7484  sdomel  7745  ackbij1lem16  8691  ltapr  9496  rpnnen1lem5  11323  qbtwnre  11521  om2uzlt2i  12197  m1dvdsndvds  14798  pcpremul  14842  pcaddlem  14882  pockthlem  14898  prmreclem6  14914  catidd  15635  ghmf1  16960  gexdvds  17284  sylow1lem1  17299  lt6abl  17578  ablfacrplem  17747  drnginvrn0  18042  issrngd  18138  islssd  18208  znrrg  19185  isphld  19270  cnllycmp  22033  nmhmcn  22183  minveclem7  22426  minveclem7OLD  22438  ioorcl2  22573  itg2seq  22749  dvlip2  22996  mdegmullem  23076  plyco0  23195  pilem3  23458  pilem3OLD  23459  sincosq1sgn  23502  sincosq2sgn  23503  logcj  23604  argimgt0  23610  lgseisenlem2  24327  eengtrkg  25064  eengtrkge  25065  ubthlem2  26562  minvecolem7  26574  minvecolem7OLD  26584  nmcexi  27728  lnconi  27735  pjnormssi  27870  tan2h  31982  itg2gt0cn  32042  divrngcl  32241  lshpcmp  32599  cdlemk35s  34549  cdlemk39s  34551  cdlemk42  34553  dihlspsnat  34946  clcnvlem  36275
  Copyright terms: Public domain W3C validator