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 238	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 260	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  tz6.12i  6920  f1imass  7263  focdmex  7942  tposfn2  8233  naddel1  8686  eroveu  8806  sdomel  9124  ackbij1lem16  10230  ltapr  11040  rpnnen1lem5  12965  qbtwnre  13178  om2uzlt2i  13916  m1dvdsndvds  16731  pcpremul  16776  pcaddlem  16821  pockthlem  16838  prmreclem6  16854  catidd  17624  issgrpd  18621  ghmf1  19121  gexdvds  19452  sylow1lem1  19466  lt6abl  19763  ablfacrplem  19935  drnginvrn0  20380  issrngd  20469  islssd  20546  isdomn4  20918  znrrg  21121  isphld  21207  cnllycmp  24472  nmhmcn  24636  minveclem7  24952  ioorcl2  25089  itg2seq  25260  dvlip2  25512  mdegmullem  25596  plyco0  25706  sincosq1sgn  26008  sincosq2sgn  26009  logcj  26114  argimgt0  26120  lgseisenlem2  26879  sleadd1im  27473  sleadd1  27475  sltonold  27690  eengtrkg  28275  eengtrkge  28276  ubthlem2  30155  minvecolem7  30167  nmcexi  31310  lnconi  31317  pjnormssi  31452  opsbc2ie  31747  qusvscpbl  32497  tan2h  36528  lindsadd  36529  itg2gt0cn  36591  divrngcl  36873  lshpcmp  37906  cdlemk35s  39856  cdlemk39s  39858  cdlemk42  39860  dihlspsnat  40252  clcnvlem  42422  tz6.12i-afv2  45999  sqrtnegnre  46063