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

Theorem 3imtr3d 282
Description: More general version of 3imtr3i 280. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
Hypotheses
Ref Expression
3imtr3d.1 (𝜑 → (𝜓𝜒))
3imtr3d.2 (𝜑 → (𝜓𝜃))
3imtr3d.3 (𝜑 → (𝜒𝜏))
Assertion
Ref Expression
3imtr3d (𝜑 → (𝜃𝜏))

Proof of Theorem 3imtr3d
StepHypRef Expression
1 3imtr3d.2 . 2 (𝜑 → (𝜓𝜃))
2 3imtr3d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3imtr3d.3 . . 3 (𝜑 → (𝜒𝜏))
42, 3sylibd 229 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 250 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  tz6.12i  6181  f1imass  6486  fornex  7097  tposfn2  7334  eroveu  7802  sdomel  8067  ackbij1lem16  9017  ltapr  9827  rpnnen1lem5  11778  rpnnen1lem5OLD  11784  qbtwnre  11989  om2uzlt2i  12706  m1dvdsndvds  15446  pcpremul  15491  pcaddlem  15535  pockthlem  15552  prmreclem6  15568  catidd  16281  ghmf1  17629  gexdvds  17939  sylow1lem1  17953  lt6abl  18236  ablfacrplem  18404  drnginvrn0  18705  issrngd  18801  islssd  18876  znrrg  19854  isphld  19939  cnllycmp  22695  nmhmcn  22860  minveclem7  23146  ioorcl2  23280  itg2seq  23449  dvlip2  23696  mdegmullem  23776  plyco0  23886  pilem3  24145  sincosq1sgn  24188  sincosq2sgn  24189  logcj  24290  argimgt0  24296  lgseisenlem2  25035  eengtrkg  25799  eengtrkge  25800  ubthlem2  27615  minvecolem7  27627  nmcexi  28773  lnconi  28780  pjnormssi  28915  tan2h  33072  itg2gt0cn  33136  divrngcl  33427  lshpcmp  33794  cdlemk35s  35744  cdlemk39s  35746  cdlemk42  35748  dihlspsnat  36141  clcnvlem  37450
  Copyright terms: Public domain W3C validator