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

Theorem 3imtr3d 296
Description: More general version of 3imtr3i 294. 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 242 . 2 (𝜑 → (𝜓𝜏))
51, 4sylbird 263 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  tz6.12i  6679  f1imass  7006  fornex  7642  tposfn2  7899  eroveu  8377  sdomel  8650  ackbij1lem16  9644  ltapr  10454  rpnnen1lem5  12368  qbtwnre  12580  om2uzlt2i  13314  m1dvdsndvds  16124  pcpremul  16169  pcaddlem  16213  pockthlem  16230  prmreclem6  16246  catidd  16942  ghmf1  18378  gexdvds  18700  sylow1lem1  18714  lt6abl  19006  ablfacrplem  19178  drnginvrn0  19508  issrngd  19620  islssd  19695  znrrg  20700  isphld  20786  cnllycmp  23552  nmhmcn  23716  minveclem7  24030  ioorcl2  24167  itg2seq  24337  dvlip2  24589  mdegmullem  24670  plyco0  24780  sincosq1sgn  25082  sincosq2sgn  25083  logcj  25188  argimgt0  25194  lgseisenlem2  25951  eengtrkg  26771  eengtrkge  26772  ubthlem2  28645  minvecolem7  28657  nmcexi  29800  lnconi  29807  pjnormssi  29942  opsbc2ie  30236  qusvscpbl  30940  tan2h  34954  lindsadd  34955  itg2gt0cn  35017  divrngcl  35300  lshpcmp  36189  cdlemk35s  38138  cdlemk39s  38140  cdlemk42  38142  dihlspsnat  38534  clcnvlem  40170  tz6.12i-afv2  43656  sqrtnegnre  43721
  Copyright terms: Public domain W3C validator