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  6866  f1imass  7219  focdmex  7909  tposfn2  8198  naddel1  8623  eroveu  8759  sdomel  9062  ackbij1lem16  10156  ltapr  10968  rpnnen1lem5  12931  qbtwnre  13151  om2uzlt2i  13913  m1dvdsndvds  16769  pcpremul  16814  pcaddlem  16859  pockthlem  16876  prmreclem6  16892  catidd  17646  issgrpd  18698  ghmf1  19221  gexdvds  19559  sylow1lem1  19573  lt6abl  19870  ablfacrplem  20042  isdomn4  20693  drnginvrn0  20731  issrngd  20832  islssd  20930  znrrg  21545  isphld  21634  cnllycmp  24923  nmhmcn  25087  minveclem7  25402  ioorcl2  25539  itg2seq  25709  dvlip2  25962  mdegmullem  26043  plyco0  26157  sincosq1sgn  26462  sincosq2sgn  26463  logcj  26570  argimgt0  26576  lgseisenlem2  27339  leadds1im  27979  leadds1  27981  ltonold  28253  onnolt  28258  addonbday  28271  om2noseqlt2  28292  bdaypw2n0bndlem  28455  remulscllem2  28493  eengtrkg  29055  eengtrkge  29056  ubthlem2  30942  minvecolem7  30954  nmcexi  32097  lnconi  32104  pjnormssi  32239  opsbc2ie  32545  qusvscpbl  33411  tan2h  37933  lindsadd  37934  itg2gt0cn  37996  divrngcl  38278  lshpcmp  39434  cdlemk35s  41383  cdlemk39s  41385  cdlemk42  41387  dihlspsnat  41779  clcnvlem  44050  tz6.12i-afv2  47691  sqrtnegnre  47755