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
3imtr3d.2
3imtr3d.3

Assertion

Ref	Expression
3imtr3d

Proof of Theorem 3imtr3d

Step	Hyp	Ref	Expression
1		3imtr3d.2	. 2
2		3imtr3d.1	. . 3
3		3imtr3d.3	. . 3
4	2, 3	sylibd 214	. 2
5	1, 4	sylbird 235	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  tz6.12i  5891  f1imass  6172  fornex  6769  tposfn2  6996  eroveu  7425  sdomel  7684  ackbij1lem16  8636  ltapr  9444  rpnnen1lem5  11241  qbtwnre  11427  om2uzlt2i  12062  m1dvdsndvds  14325  pcpremul  14367  pcaddlem  14407  pockthlem  14423  prmreclem6  14439  catidd  15077  ghmf1  16295  gexdvds  16604  sylow1lem1  16618  lt6abl  16897  ablfacrplem  17116  drnginvrn0  17414  issrngd  17510  islssd  17582  znrrg  18604  isphld  18689  cnllycmp  21456  nmhmcn  21603  minveclem7  21850  ioorcl2  21981  itg2seq  22149  dvlip2  22396  mdegmullem  22478  plyco0  22589  pilem3  22848  sincosq1sgn  22891  sincosq2sgn  22892  logcj  22991  argimgt0  22997  lgseisenlem2  23625  eengtrkg  24288  eengtrkge  24289  ubthlem2  25787  minvecolem7  25799  nmcexi  26945  lnconi  26952  pjnormssi  27087  tan2h  30047  itg2gt0cn  30070  divrngcl  30360  lshpcmp  34713  cdlemk35s  36663  cdlemk39s  36665  cdlemk42  36667  dihlspsnat  37060

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