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

Theorem 3imtr3d 259
Description: More general version of 3imtr3i 257. 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 206 . 2  |-  ( ph  ->  ( ps  ->  ta ) )
51, 4sylbird 227 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  tz6.12i  5751  fornex  5970  f1imass  6010  tposfn2  6501  eroveu  6999  sdomel  7254  ackbij1lem16  8115  ltapr  8922  rpnnen1lem5  10604  qbtwnre  10785  om2uzlt2i  11291  pcpremul  13217  pcaddlem  13257  pockthlem  13273  prmreclem6  13289  catidd  13905  ghmf1  15034  gexdvds  15218  sylow1lem1  15232  lt6abl  15504  ablfacrplem  15623  drnginvrn0  15853  issrngd  15949  islssd  16012  znrrg  16846  isphld  16885  cnllycmp  18981  nmhmcn  19128  minveclem7  19336  ioorcl2  19464  itg2seq  19634  dvlip2  19879  mdegmullem  20001  plyco0  20111  pilem3  20369  sincosq1sgn  20406  sincosq2sgn  20407  logcj  20501  argimgt0  20507  lgseisenlem2  21134  ubthlem2  22373  minvecolem7  22385  nmcexi  23529  lnconi  23536  pjnormssi  23671  itg2gt0cn  26260  divrngcl  26573  lshpcmp  29786  cdlemk35s  31734  cdlemk39s  31736  cdlemk42  31738  dihlspsnat  32131
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 178
  Copyright terms: Public domain W3C validator