Theorem 3imtr3d 296

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  tz6.12i  6942  f1imass  7299  focdmex  8002  tposfn2  8303  naddel1  8735  eroveu  8871  sdomel  9181  ackbij1lem16  10351  ltapr  11169  rpnnen1lem5  13149  qbtwnre  13369  om2uzlt2i  14134  m1dvdsndvds  17020  pcpremul  17065  pcaddlem  17110  pockthlem  17127  prmreclem6  17143  catidd  17904  issgrpd  18969  ghmf1  19510  gexdvds  19849  sylow1lem1  19863  lt6abl  20160  ablfacrplem  20332  isdomn4  21018  drnginvrn0  21063  issrngd  21163  islssd  21261  znrrg  21926  isphld  22015  cnllycmp  25332  nmhmcn  25496  minveclem7  25811  ioorcl2  25948  itg2seq  26118  dvlip2  26370  mdegmullem  26451  plyco0  26565  sincosq1sgn  26884  sincosq2sgn  26885  logcj  26991  argimgt0  26997  lgseisenlem2  27760  leadds1im  28430  leadds1  28432  ltonold  28704  onnolt  28709  addonbday  28722  om2noseqlt2  28743  bdaypw2n0bndlem  28906  remulscllem2  28944  eengtrkg  29621  eengtrkge  29622  ubthlem2  31530  minvecolem7  31542  nmcexi  32685  lnconi  32692  pjnormssi  32827  opsbc2ie  33171  qusvscpbl  34016  tan2h  38803  lindsadd  38804  itg2gt0cn  38861  divrngcl  39157  lshpcmp  40311  cdlemk35s  42260  cdlemk39s  42262  cdlemk42  42264  dihlspsnat  42656  clcnvlem  44884  hashnnltb  46277  tz6.12i-afv2  48586  sqrtnegnre  48650