Theorem 3imtr3d 295

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  tz6.12i  6889  f1imass  7244  focdmex  7933  tposfn2  8223  naddel1  8653  eroveu  8789  sdomel  9092  ackbij1lem16  10187  ltapr  11000  rpnnen1lem5  12979  qbtwnre  13199  om2uzlt2i  13961  m1dvdsndvds  16817  pcpremul  16862  pcaddlem  16907  pockthlem  16924  prmreclem6  16940  catidd  17695  issgrpd  18747  ghmf1  19269  gexdvds  19607  sylow1lem1  19621  lt6abl  19918  ablfacrplem  20090  isdomn4  20745  drnginvrn0  20783  issrngd  20884  islssd  20982  znrrg  21597  isphld  21686  cnllycmp  24998  nmhmcn  25162  minveclem7  25477  ioorcl2  25614  itg2seq  25784  dvlip2  26037  mdegmullem  26118  plyco0  26232  sincosq1sgn  26540  sincosq2sgn  26541  logcj  26648  argimgt0  26654  lgseisenlem2  27417  leadds1im  28057  leadds1  28059  ltonold  28331  onnolt  28336  addonbday  28349  om2noseqlt2  28370  bdaypw2n0bndlem  28533  remulscllem2  28571  eengtrkg  29133  eengtrkge  29134  ubthlem2  31020  minvecolem7  31032  nmcexi  32175  lnconi  32182  pjnormssi  32317  opsbc2ie  32623  qusvscpbl  33498  tan2h  38075  lindsadd  38076  itg2gt0cn  38138  divrngcl  38420  lshpcmp  39576  cdlemk35s  41525  cdlemk39s  41527  cdlemk42  41529  dihlspsnat  41921  clcnvlem  44163  tz6.12i-afv2  47801  sqrtnegnre  47865