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  5548  fornex  5750  f1imass  5788  tposfn2  6256  eroveu  6753  sdomel  7008  ltapr  8669  rpnnen1lem5  10346  qbtwnre  10526  om2uzlt2i  11014  pcpremul  12896  pcaddlem  12936  pockthlem  12952  prmreclem6  12968  catidd  13582  ghmf1  14711  gexdvds  14895  sylow1lem1  14909  lt6abl  15181  ablfacrplem  15300  drnginvrn0  15530  issrngd  15626  islssd  15693  znrrg  16519  isphld  16558  cnllycmp  18454  nmhmcn  18601  minveclem7  18799  ioorcl2  18927  itg2seq  19097  dvlip2  19342  mdegmullem  19464  plyco0  19574  pilem3  19829  sincosq1sgn  19866  sincosq2sgn  19867  logcj  19960  argimgt0  19966  lgseisenlem2  20589  ubthlem2  21450  minvecolem7  21462  nmcexi  22606  lnconi  22613  pjnormssi  22748  divrngcl  26588  lshpcmp  29178  cdlemk35s  31126  cdlemk39s  31128  cdlemk42  31130  dihlspsnat  31523
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