Theorem 3imtr3d 292

Description: More general version of 3imtr3i 290. 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 259	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  6918  f1imass  7265  focdmex  7944  tposfn2  8235  naddel1  8688  eroveu  8808  sdomel  9126  ackbij1lem16  10232  ltapr  11042  rpnnen1lem5  12969  qbtwnre  13182  om2uzlt2i  13920  m1dvdsndvds  16735  pcpremul  16780  pcaddlem  16825  pockthlem  16842  prmreclem6  16858  catidd  17628  issgrpd  18655  ghmf1  19160  gexdvds  19493  sylow1lem1  19507  lt6abl  19804  ablfacrplem  19976  drnginvrn0  20523  issrngd  20612  islssd  20690  isdomn4  21118  znrrg  21340  isphld  21426  cnllycmp  24702  nmhmcn  24867  minveclem7  25183  ioorcl2  25321  itg2seq  25492  dvlip2  25747  mdegmullem  25831  plyco0  25941  sincosq1sgn  26244  sincosq2sgn  26245  logcj  26350  argimgt0  26356  lgseisenlem2  27115  sleadd1im  27709  sleadd1  27711  sltonold  27926  eengtrkg  28511  eengtrkge  28512  ubthlem2  30391  minvecolem7  30403  nmcexi  31546  lnconi  31553  pjnormssi  31688  opsbc2ie  31983  qusvscpbl  32736  tan2h  36783  lindsadd  36784  itg2gt0cn  36846  divrngcl  37128  lshpcmp  38161  cdlemk35s  40111  cdlemk39s  40113  cdlemk42  40115  dihlspsnat  40507  clcnvlem  42676  tz6.12i-afv2  46249  sqrtnegnre  46313