Theorem 3imtr3d 285

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  tz6.12i  6437  f1imass  6749  fornex  7370  tposfn2  7612  eroveu  8081  sdomel  8349  ackbij1lem16  9345  ltapr  10155  rpnnen1lem5  12065  qbtwnre  12279  om2uzlt2i  13005  m1dvdsndvds  15836  pcpremul  15881  pcaddlem  15925  pockthlem  15942  prmreclem6  15958  catidd  16655  ghmf1  18002  gexdvds  18312  sylow1lem1  18326  lt6abl  18611  ablfacrplem  18780  drnginvrn0  19083  issrngd  19179  islssd  19254  znrrg  20235  isphld  20323  cnllycmp  23083  nmhmcn  23247  minveclem7  23545  ioorcl2  23680  itg2seq  23850  dvlip2  24099  mdegmullem  24179  plyco0  24289  pilem3OLD  24549  sincosq1sgn  24592  sincosq2sgn  24593  logcj  24693  argimgt0  24699  lgseisenlem2  25453  eengtrkg  26222  eengtrkge  26223  ubthlem2  28252  minvecolem7  28264  nmcexi  29410  lnconi  29417  pjnormssi  29552  tan2h  33890  itg2gt0cn  33953  divrngcl  34243  lshpcmp  35009  cdlemk35s  36958  cdlemk39s  36960  cdlemk42  36962  dihlspsnat  37354  clcnvlem  38713  tz6.12i-afv2  42097