Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imtr3d 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
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 206 . 2
51, 4sylbird 227 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177 This theorem is referenced by:  tz6.12i  5705  fornex  5923  f1imass  5963  tposfn2  6451  eroveu  6949  sdomel  7204  ackbij1lem16  8062  ltapr  8869  rpnnen1lem5  10550  qbtwnre  10731  om2uzlt2i  11232  pcpremul  13158  pcaddlem  13198  pockthlem  13214  prmreclem6  13230  catidd  13846  ghmf1  14975  gexdvds  15159  sylow1lem1  15173  lt6abl  15445  ablfacrplem  15564  drnginvrn0  15794  issrngd  15890  islssd  15953  znrrg  16783  isphld  16822  cnllycmp  18866  nmhmcn  19013  minveclem7  19217  ioorcl2  19345  itg2seq  19515  dvlip2  19760  mdegmullem  19882  plyco0  19992  pilem3  20250  sincosq1sgn  20287  sincosq2sgn  20288  logcj  20382  argimgt0  20388  lgseisenlem2  21015  ubthlem2  22235  minvecolem7  22247  nmcexi  23391  lnconi  23398  pjnormssi  23533  itg2gt0cn  25976  divrngcl  26280  lshpcmp  29119  cdlemk35s  31067  cdlemk39s  31069  cdlemk42  31071  dihlspsnat  31464 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