Theorem 3imtr3d 293

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  tz6.12i  6860  f1imass  7212  focdmex  7902  tposfn2  8191  naddel1  8616  eroveu  8752  sdomel  9055  ackbij1lem16  10147  ltapr  10959  rpnnen1lem5  12922  qbtwnre  13142  om2uzlt2i  13904  m1dvdsndvds  16760  pcpremul  16805  pcaddlem  16850  pockthlem  16867  prmreclem6  16883  catidd  17637  issgrpd  18689  ghmf1  19212  gexdvds  19550  sylow1lem1  19564  lt6abl  19861  ablfacrplem  20033  isdomn4  20684  drnginvrn0  20722  issrngd  20823  islssd  20921  znrrg  21555  isphld  21644  cnllycmp  24933  nmhmcn  25097  minveclem7  25412  ioorcl2  25549  itg2seq  25719  dvlip2  25972  mdegmullem  26053  plyco0  26167  sincosq1sgn  26475  sincosq2sgn  26476  logcj  26583  argimgt0  26589  lgseisenlem2  27353  leadds1im  27993  leadds1  27995  ltonold  28267  onnolt  28272  addonbday  28285  om2noseqlt2  28306  bdaypw2n0bndlem  28469  remulscllem2  28507  eengtrkg  29069  eengtrkge  29070  ubthlem2  30957  minvecolem7  30969  nmcexi  32112  lnconi  32119  pjnormssi  32254  opsbc2ie  32560  qusvscpbl  33426  tan2h  37947  lindsadd  37948  itg2gt0cn  38010  divrngcl  38292  lshpcmp  39448  cdlemk35s  41397  cdlemk39s  41399  cdlemk42  41401  dihlspsnat  41793  clcnvlem  44068  tz6.12i-afv2  47703  sqrtnegnre  47767