Theorem 3imtr3d 294

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  tz6.12i  6860  f1imass  7215  focdmex  7905  tposfn2  8195  naddel1  8620  eroveu  8756  sdomel  9059  ackbij1lem16  10154  ltapr  10966  rpnnen1lem5  12929  qbtwnre  13149  om2uzlt2i  13911  m1dvdsndvds  16767  pcpremul  16812  pcaddlem  16857  pockthlem  16874  prmreclem6  16890  catidd  17644  issgrpd  18696  ghmf1  19219  gexdvds  19557  sylow1lem1  19571  lt6abl  19868  ablfacrplem  20040  isdomn4  20695  drnginvrn0  20733  issrngd  20834  islssd  20932  znrrg  21547  isphld  21636  cnllycmp  24948  nmhmcn  25112  minveclem7  25427  ioorcl2  25564  itg2seq  25734  dvlip2  25987  mdegmullem  26068  plyco0  26182  sincosq1sgn  26487  sincosq2sgn  26488  logcj  26595  argimgt0  26601  lgseisenlem2  27364  leadds1im  28004  leadds1  28006  ltonold  28278  onnolt  28283  addonbday  28296  om2noseqlt2  28317  bdaypw2n0bndlem  28480  remulscllem2  28518  eengtrkg  29080  eengtrkge  29081  ubthlem2  30967  minvecolem7  30979  nmcexi  32122  lnconi  32129  pjnormssi  32264  opsbc2ie  32570  qusvscpbl  33441  tan2h  37986  lindsadd  37987  itg2gt0cn  38049  divrngcl  38331  lshpcmp  39487  cdlemk35s  41436  cdlemk39s  41438  cdlemk42  41440  dihlspsnat  41832  clcnvlem  44074  tz6.12i-afv2  47713  sqrtnegnre  47777