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  6700  f1imass  7033  fornex  7682  tposfn2  7943  eroveu  8423  sdomel  8714  ackbij1lem16  9735  ltapr  10545  rpnnen1lem5  12463  qbtwnre  12675  om2uzlt2i  13410  m1dvdsndvds  16235  pcpremul  16280  pcaddlem  16324  pockthlem  16341  prmreclem6  16357  catidd  17054  ghmf1  18505  gexdvds  18827  sylow1lem1  18841  lt6abl  19134  ablfacrplem  19306  drnginvrn0  19639  issrngd  19751  islssd  19826  znrrg  20384  isphld  20470  cnllycmp  23708  nmhmcn  23872  minveclem7  24187  ioorcl2  24324  itg2seq  24495  dvlip2  24747  mdegmullem  24831  plyco0  24941  sincosq1sgn  25243  sincosq2sgn  25244  logcj  25349  argimgt0  25355  lgseisenlem2  26112  eengtrkg  26932  eengtrkge  26933  ubthlem2  28806  minvecolem7  28818  nmcexi  29961  lnconi  29968  pjnormssi  30103  opsbc2ie  30398  qusvscpbl  31123  naddel1  33480  tan2h  35392  lindsadd  35393  itg2gt0cn  35455  divrngcl  35738  lshpcmp  36625  cdlemk35s  38574  cdlemk39s  38576  cdlemk42  38578  dihlspsnat  38970  isdomn4  39763  clcnvlem  40776  tz6.12i-afv2  44268  sqrtnegnre  44333