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  12996  qbtwnre  13216  om2uzlt2i  13978  m1dvdsndvds  16848  pcpremul  16893  pcaddlem  16938  pockthlem  16955  prmreclem6  16971  catidd  17726  issgrpd  18778  ghmf1  19307  gexdvds  19645  sylow1lem1  19659  lt6abl  19956  ablfacrplem  20128  isdomn4  20791  drnginvrn0  20828  issrngd  20927  islssd  21025  znrrg  21675  isphld  21764  cnllycmp  25076  nmhmcn  25240  minveclem7  25555  ioorcl2  25692  itg2seq  25862  dvlip2  26115  mdegmullem  26196  plyco0  26310  sincosq1sgn  26621  sincosq2sgn  26622  logcj  26729  argimgt0  26735  lgseisenlem2  27498  leadds1im  28138  leadds1  28140  ltonold  28412  onnolt  28417  addonbday  28430  om2noseqlt2  28451  bdaypw2n0bndlem  28614  remulscllem2  28652  eengtrkg  29245  eengtrkge  29246  ubthlem2  31132  minvecolem7  31144  nmcexi  32287  lnconi  32294  pjnormssi  32429  opsbc2ie  32732  qusvscpbl  33586  tan2h  38123  lindsadd  38124  itg2gt0cn  38186  divrngcl  38468  lshpcmp  39624  cdlemk35s  41573  cdlemk39s  41575  cdlemk42  41577  dihlspsnat  41969  clcnvlem  44211  tz6.12i-afv2  47835  sqrtnegnre  47899