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  6852  f1imass  7205  focdmex  7898  tposfn2  8188  naddel1  8612  eroveu  8746  sdomel  9048  ackbij1lem16  10147  ltapr  10958  rpnnen1lem5  12900  qbtwnre  13119  om2uzlt2i  13876  m1dvdsndvds  16728  pcpremul  16773  pcaddlem  16818  pockthlem  16835  prmreclem6  16851  catidd  17604  issgrpd  18622  ghmf1  19143  gexdvds  19481  sylow1lem1  19495  lt6abl  19792  ablfacrplem  19964  isdomn4  20619  drnginvrn0  20657  issrngd  20758  islssd  20856  znrrg  21490  isphld  21579  cnllycmp  24871  nmhmcn  25036  minveclem7  25351  ioorcl2  25489  itg2seq  25659  dvlip2  25916  mdegmullem  25999  plyco0  26113  sincosq1sgn  26423  sincosq2sgn  26424  logcj  26531  argimgt0  26537  lgseisenlem2  27303  sleadd1im  27917  sleadd1  27919  sltonold  28185  onnolt  28190  om2noseqlt2  28217  remulscllem2  28388  eengtrkg  28949  eengtrkge  28950  ubthlem2  30833  minvecolem7  30845  nmcexi  31988  lnconi  31995  pjnormssi  32130  opsbc2ie  32438  qusvscpbl  33301  tan2h  37594  lindsadd  37595  itg2gt0cn  37657  divrngcl  37939  lshpcmp  38969  cdlemk35s  40919  cdlemk39s  40921  cdlemk42  40923  dihlspsnat  41315  clcnvlem  43599  tz6.12i-afv2  47231  sqrtnegnre  47295