Theorem 3imtr3d 281

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  tz6.12i  6124  f1imass  6422  fornex  7028  tposfn2  7261  eroveu  7729  sdomel  7992  ackbij1lem16  8940  ltapr  9746  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  qbtwnre  11904  om2uzlt2i  12612  m1dvdsndvds  15341  pcpremul  15386  pcaddlem  15430  pockthlem  15447  prmreclem6  15463  catidd  16164  ghmf1  17512  gexdvds  17822  sylow1lem1  17836  lt6abl  18119  ablfacrplem  18287  drnginvrn0  18588  issrngd  18684  islssd  18757  znrrg  19733  isphld  19818  cnllycmp  22563  nmhmcn  22728  minveclem7  23014  ioorcl2  23146  itg2seq  23315  dvlip2  23562  mdegmullem  23642  plyco0  23752  pilem3  24011  sincosq1sgn  24054  sincosq2sgn  24055  logcj  24156  argimgt0  24162  lgseisenlem2  24901  eengtrkg  25665  eengtrkge  25666  ubthlem2  27111  minvecolem7  27123  nmcexi  28269  lnconi  28276  pjnormssi  28411  tan2h  32571  itg2gt0cn  32635  divrngcl  32926  lshpcmp  33293  cdlemk35s  35243  cdlemk39s  35245  cdlemk42  35247  dihlspsnat  35640  clcnvlem  36949