Theorem 3imtr3d 293

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  tz6.12i  6886  f1imass  7239  focdmex  7934  tposfn2  8227  naddel1  8651  eroveu  8785  sdomel  9088  ackbij1lem16  10187  ltapr  10998  rpnnen1lem5  12940  qbtwnre  13159  om2uzlt2i  13916  m1dvdsndvds  16769  pcpremul  16814  pcaddlem  16859  pockthlem  16876  prmreclem6  16892  catidd  17641  issgrpd  18657  ghmf1  19178  gexdvds  19514  sylow1lem1  19528  lt6abl  19825  ablfacrplem  19997  isdomn4  20625  drnginvrn0  20663  issrngd  20764  islssd  20841  znrrg  21475  isphld  21563  cnllycmp  24855  nmhmcn  25020  minveclem7  25335  ioorcl2  25473  itg2seq  25643  dvlip2  25900  mdegmullem  25983  plyco0  26097  sincosq1sgn  26407  sincosq2sgn  26408  logcj  26515  argimgt0  26521  lgseisenlem2  27287  sleadd1im  27894  sleadd1  27896  sltonold  28162  onnolt  28167  om2noseqlt2  28194  remulscllem2  28352  eengtrkg  28913  eengtrkge  28914  ubthlem2  30800  minvecolem7  30812  nmcexi  31955  lnconi  31962  pjnormssi  32097  opsbc2ie  32405  qusvscpbl  33322  tan2h  37606  lindsadd  37607  itg2gt0cn  37669  divrngcl  37951  lshpcmp  38981  cdlemk35s  40931  cdlemk39s  40933  cdlemk42  40935  dihlspsnat  41327  clcnvlem  43612  tz6.12i-afv2  47244  sqrtnegnre  47308