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  6911  f1imass  7264  focdmex  7955  tposfn2  8246  naddel1  8676  eroveu  8812  sdomel  9115  ackbij1lem16  10229  ltapr  11041  rpnnen1lem5  13016  qbtwnre  13236  om2uzlt2i  14000  m1dvdsndvds  16875  pcpremul  16920  pcaddlem  16965  pockthlem  16982  prmreclem6  16998  catidd  17753  issgrpd  18809  ghmf1  19339  gexdvds  19677  sylow1lem1  19691  lt6abl  19988  ablfacrplem  20160  isdomn4  20843  drnginvrn0  20887  issrngd  20987  islssd  21085  znrrg  21744  isphld  21833  cnllycmp  25144  nmhmcn  25308  minveclem7  25623  ioorcl2  25760  itg2seq  25930  dvlip2  26183  mdegmullem  26264  plyco0  26378  sincosq1sgn  26692  sincosq2sgn  26693  logcj  26800  argimgt0  26806  lgseisenlem2  27569  leadds1im  28209  leadds1  28211  ltonold  28483  onnolt  28488  addonbday  28501  om2noseqlt2  28522  bdaypw2n0bndlem  28685  remulscllem2  28723  eengtrkg  29365  eengtrkge  29366  ubthlem2  31252  minvecolem7  31264  nmcexi  32407  lnconi  32414  pjnormssi  32549  opsbc2ie  32851  qusvscpbl  33694  tan2h  38296  lindsadd  38297  itg2gt0cn  38359  divrngcl  38641  lshpcmp  39795  cdlemk35s  41744  cdlemk39s  41746  cdlemk42  41748  dihlspsnat  42140  clcnvlem  44382  hashnnltb  45765  tz6.12i-afv2  48013  sqrtnegnre  48077