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  6363  f1imass  6672  fornex  7288  tposfn2  7531  eroveu  7997  sdomel  8260  ackbij1lem16  9220  ltapr  10030  rpnnen1lem5  11982  rpnnen1lem5OLD  11988  qbtwnre  12194  om2uzlt2i  12915  m1dvdsndvds  15676  pcpremul  15721  pcaddlem  15765  pockthlem  15782  prmreclem6  15798  catidd  16513  ghmf1  17861  gexdvds  18170  sylow1lem1  18184  lt6abl  18467  ablfacrplem  18635  drnginvrn0  18938  issrngd  19034  islssd  19109  znrrg  20087  isphld  20172  cnllycmp  22927  nmhmcn  23091  minveclem7  23377  ioorcl2  23511  itg2seq  23679  dvlip2  23928  mdegmullem  24008  plyco0  24118  pilem3  24377  sincosq1sgn  24420  sincosq2sgn  24421  logcj  24522  argimgt0  24528  lgseisenlem2  25271  eengtrkg  26035  eengtrkge  26036  ubthlem2  28007  minvecolem7  28019  nmcexi  29165  lnconi  29172  pjnormssi  29307  tan2h  33683  itg2gt0cn  33747  divrngcl  34038  lshpcmp  34747  cdlemk35s  36696  cdlemk39s  36698  cdlemk42  36700  dihlspsnat  37093  clcnvlem  38401
  Copyright terms: Public domain W3C validator