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  5564  fornex  5766  f1imass  5804  tposfn2  6272  eroveu  6769  sdomel  7024  ltapr  8685  rpnnen1lem5  10362  qbtwnre  10542  om2uzlt2i  11030  pcpremul  12912  pcaddlem  12952  pockthlem  12968  prmreclem6  12984  catidd  13598  ghmf1  14727  gexdvds  14911  sylow1lem1  14925  lt6abl  15197  ablfacrplem  15316  drnginvrn0  15546  issrngd  15642  islssd  15709  znrrg  16535  isphld  16574  cnllycmp  18470  nmhmcn  18617  minveclem7  18815  ioorcl2  18943  itg2seq  19113  dvlip2  19358  mdegmullem  19480  plyco0  19590  pilem3  19845  sincosq1sgn  19882  sincosq2sgn  19883  logcj  19976  argimgt0  19982  lgseisenlem2  20605  ubthlem2  21466  minvecolem7  21478  nmcexi  22622  lnconi  22629  pjnormssi  22764  itg2gt0cn  25006  divrngcl  26691  lshpcmp  29800  cdlemk35s  31748  cdlemk39s  31750  cdlemk42  31752  dihlspsnat  32145
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