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  6860  f1imass  7210  focdmex  7900  tposfn2  8190  naddel1  8615  eroveu  8749  sdomel  9052  ackbij1lem16  10144  ltapr  10956  rpnnen1lem5  12894  qbtwnre  13114  om2uzlt2i  13874  m1dvdsndvds  16726  pcpremul  16771  pcaddlem  16816  pockthlem  16833  prmreclem6  16849  catidd  17603  issgrpd  18655  ghmf1  19175  gexdvds  19513  sylow1lem1  19527  lt6abl  19824  ablfacrplem  19996  isdomn4  20649  drnginvrn0  20687  issrngd  20788  islssd  20886  znrrg  21520  isphld  21609  cnllycmp  24911  nmhmcn  25076  minveclem7  25391  ioorcl2  25529  itg2seq  25699  dvlip2  25956  mdegmullem  26039  plyco0  26153  sincosq1sgn  26463  sincosq2sgn  26464  logcj  26571  argimgt0  26577  lgseisenlem2  27343  leadds1im  27983  leadds1  27985  ltonold  28257  onnolt  28262  addonbday  28275  om2noseqlt2  28296  bdaypw2n0bndlem  28459  remulscllem2  28497  eengtrkg  29059  eengtrkge  29060  ubthlem2  30946  minvecolem7  30958  nmcexi  32101  lnconi  32108  pjnormssi  32243  opsbc2ie  32550  qusvscpbl  33432  tan2h  37809  lindsadd  37810  itg2gt0cn  37872  divrngcl  38154  lshpcmp  39244  cdlemk35s  41193  cdlemk39s  41195  cdlemk42  41197  dihlspsnat  41589  clcnvlem  43860  tz6.12i-afv2  47485  sqrtnegnre  47549