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  5884  f1imass  6158  fornex  6750  tposfn2  6974  eroveu  7403  sdomel  7661  ackbij1lem16  8611  ltapr  9419  rpnnen1lem5  11208  qbtwnre  11394  om2uzlt2i  12026  m1dvdsndvds  14180  pcpremul  14222  pcaddlem  14262  pockthlem  14278  prmreclem6  14294  catidd  14931  ghmf1  16090  gexdvds  16400  sylow1lem1  16414  lt6abl  16688  ablfacrplem  16906  drnginvrn0  17197  issrngd  17293  islssd  17365  znrrg  18371  isphld  18456  cnllycmp  21191  nmhmcn  21338  minveclem7  21585  ioorcl2  21716  itg2seq  21884  dvlip2  22131  mdegmullem  22213  plyco0  22324  pilem3  22582  sincosq1sgn  22624  sincosq2sgn  22625  logcj  22719  argimgt0  22725  lgseisenlem2  23353  ubthlem2  25463  minvecolem7  25475  nmcexi  26621  lnconi  26628  pjnormssi  26763  tan2h  29624  itg2gt0cn  29647  divrngcl  29963  lshpcmp  33785  cdlemk35s  35733  cdlemk39s  35735  cdlemk42  35737  dihlspsnat  36130
  Copyright terms: Public domain W3C validator