Theorem 3imtr3d 293

Description: More general version of 3imtr3i 291. 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 239	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 260	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  tz6.12i  6868  f1imass  7220  focdmex  7910  tposfn2  8200  naddel1  8625  eroveu  8761  sdomel  9064  ackbij1lem16  10156  ltapr  10968  rpnnen1lem5  12906  qbtwnre  13126  om2uzlt2i  13886  m1dvdsndvds  16738  pcpremul  16783  pcaddlem  16828  pockthlem  16845  prmreclem6  16861  catidd  17615  issgrpd  18667  ghmf1  19187  gexdvds  19525  sylow1lem1  19539  lt6abl  19836  ablfacrplem  20008  isdomn4  20661  drnginvrn0  20699  issrngd  20800  islssd  20898  znrrg  21532  isphld  21621  cnllycmp  24923  nmhmcn  25088  minveclem7  25403  ioorcl2  25541  itg2seq  25711  dvlip2  25968  mdegmullem  26051  plyco0  26165  sincosq1sgn  26475  sincosq2sgn  26476  logcj  26583  argimgt0  26589  lgseisenlem2  27355  leadds1im  27995  leadds1  27997  ltonold  28269  onnolt  28274  addonbday  28287  om2noseqlt2  28308  bdaypw2n0bndlem  28471  remulscllem2  28509  eengtrkg  29071  eengtrkge  29072  ubthlem2  30958  minvecolem7  30970  nmcexi  32113  lnconi  32120  pjnormssi  32255  opsbc2ie  32561  qusvscpbl  33443  tan2h  37857  lindsadd  37858  itg2gt0cn  37920  divrngcl  38202  lshpcmp  39358  cdlemk35s  41307  cdlemk39s  41309  cdlemk42  41311  dihlspsnat  41703  clcnvlem  43973  tz6.12i-afv2  47597  sqrtnegnre  47661