Theorem 3imtr3d 296

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  tz6.12i  6909  f1imass  7264  focdmex  7954  tposfn2  8245  naddel1  8675  eroveu  8811  sdomel  9113  ackbij1lem16  10218  ltapr  11031  rpnnen1lem5  13006  qbtwnre  13226  om2uzlt2i  13989  m1dvdsndvds  16859  pcpremul  16904  pcaddlem  16949  pockthlem  16966  prmreclem6  16982  catidd  17737  issgrpd  18789  ghmf1  19317  gexdvds  19655  sylow1lem1  19669  lt6abl  19966  ablfacrplem  20138  isdomn4  20801  drnginvrn0  20840  issrngd  20939  islssd  21037  znrrg  21696  isphld  21785  cnllycmp  25096  nmhmcn  25260  minveclem7  25575  ioorcl2  25712  itg2seq  25882  dvlip2  26135  mdegmullem  26216  plyco0  26330  sincosq1sgn  26644  sincosq2sgn  26645  logcj  26752  argimgt0  26758  lgseisenlem2  27521  leadds1im  28161  leadds1  28163  ltonold  28435  onnolt  28440  addonbday  28453  om2noseqlt2  28474  bdaypw2n0bndlem  28637  remulscllem2  28675  eengtrkg  29317  eengtrkge  29318  ubthlem2  31204  minvecolem7  31216  nmcexi  32359  lnconi  32366  pjnormssi  32501  opsbc2ie  32803  qusvscpbl  33652  tan2h  38244  lindsadd  38245  itg2gt0cn  38307  divrngcl  38589  lshpcmp  39743  cdlemk35s  41692  cdlemk39s  41694  cdlemk42  41696  dihlspsnat  42088  clcnvlem  44332  hashnnltb  45715  tz6.12i-afv2  47963  sqrtnegnre  48027