Theorem 3imtr3d 292

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  tz6.12i  6782  f1imass  7118  fornex  7772  tposfn2  8035  eroveu  8559  sdomel  8860  ackbij1lem16  9922  ltapr  10732  rpnnen1lem5  12650  qbtwnre  12862  om2uzlt2i  13599  m1dvdsndvds  16427  pcpremul  16472  pcaddlem  16517  pockthlem  16534  prmreclem6  16550  catidd  17306  ghmf1  18778  gexdvds  19104  sylow1lem1  19118  lt6abl  19411  ablfacrplem  19583  drnginvrn0  19924  issrngd  20036  islssd  20112  znrrg  20685  isphld  20771  cnllycmp  24025  nmhmcn  24189  minveclem7  24504  ioorcl2  24641  itg2seq  24812  dvlip2  25064  mdegmullem  25148  plyco0  25258  sincosq1sgn  25560  sincosq2sgn  25561  logcj  25666  argimgt0  25672  lgseisenlem2  26429  eengtrkg  27257  eengtrkge  27258  ubthlem2  29134  minvecolem7  29146  nmcexi  30289  lnconi  30296  pjnormssi  30431  opsbc2ie  30725  qusvscpbl  31453  naddel1  33766  tan2h  35696  lindsadd  35697  itg2gt0cn  35759  divrngcl  36042  lshpcmp  36929  cdlemk35s  38878  cdlemk39s  38880  cdlemk42  38882  dihlspsnat  39274  isdomn4  40100  clcnvlem  41120  tz6.12i-afv2  44622  sqrtnegnre  44687