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  6912  f1imass  7269  focdmex  7969  tposfn2  8269  naddel1  8701  eroveu  8837  sdomel  9147  ackbij1lem16  10316  ltapr  11134  rpnnen1lem5  13113  qbtwnre  13333  om2uzlt2i  14098  m1dvdsndvds  16982  pcpremul  17027  pcaddlem  17072  pockthlem  17089  prmreclem6  17105  catidd  17860  issgrpd  18925  ghmf1  19466  gexdvds  19804  sylow1lem1  19818  lt6abl  20115  ablfacrplem  20287  isdomn4  20973  drnginvrn0  21018  issrngd  21118  islssd  21216  znrrg  21877  isphld  21966  cnllycmp  25283  nmhmcn  25447  minveclem7  25762  ioorcl2  25899  itg2seq  26069  dvlip2  26321  mdegmullem  26402  plyco0  26516  sincosq1sgn  26833  sincosq2sgn  26834  logcj  26940  argimgt0  26946  lgseisenlem2  27709  leadds1im  28379  leadds1  28381  ltonold  28653  onnolt  28658  addonbday  28671  om2noseqlt2  28692  bdaypw2n0bndlem  28855  remulscllem2  28893  eengtrkg  29570  eengtrkge  29571  ubthlem2  31479  minvecolem7  31491  nmcexi  32634  lnconi  32641  pjnormssi  32776  opsbc2ie  33120  qusvscpbl  33959  tan2h  38629  lindsadd  38630  itg2gt0cn  38687  divrngcl  38985  lshpcmp  40139  cdlemk35s  42088  cdlemk39s  42090  cdlemk42  42092  dihlspsnat  42484  clcnvlem  44717  hashnnltb  46107  tz6.12i-afv2  48407  sqrtnegnre  48471