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 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  tz6.12i  6897  f1imass  7252  focdmex  7941  tposfn2  8232  naddel1  8662  eroveu  8798  sdomel  9100  ackbij1lem16  10205  ltapr  11018  rpnnen1lem5  12993  qbtwnre  13213  om2uzlt2i  13975  m1dvdsndvds  16846  pcpremul  16891  pcaddlem  16936  pockthlem  16953  prmreclem6  16969  catidd  17724  issgrpd  18776  ghmf1  19304  gexdvds  19642  sylow1lem1  19656  lt6abl  19953  ablfacrplem  20125  isdomn4  20788  drnginvrn0  20825  issrngd  20924  islssd  21022  znrrg  21672  isphld  21761  cnllycmp  25072  nmhmcn  25236  minveclem7  25551  ioorcl2  25688  itg2seq  25858  dvlip2  26111  mdegmullem  26192  plyco0  26306  sincosq1sgn  26617  sincosq2sgn  26618  logcj  26725  argimgt0  26731  lgseisenlem2  27494  leadds1im  28134  leadds1  28136  ltonold  28408  onnolt  28413  addonbday  28426  om2noseqlt2  28447  bdaypw2n0bndlem  28610  remulscllem2  28648  eengtrkg  29241  eengtrkge  29242  ubthlem2  31128  minvecolem7  31140  nmcexi  32283  lnconi  32290  pjnormssi  32425  opsbc2ie  32728  qusvscpbl  33581  tan2h  38118  lindsadd  38119  itg2gt0cn  38181  divrngcl  38463  lshpcmp  39619  cdlemk35s  41568  cdlemk39s  41570  cdlemk42  41572  dihlspsnat  41964  clcnvlem  44206  hashnnltb  45591  tz6.12i-afv2  47836  sqrtnegnre  47900