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 238	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbird 259	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  tz6.12i  6800  f1imass  7137  fornex  7798  tposfn2  8064  eroveu  8601  sdomel  8911  ackbij1lem16  9991  ltapr  10801  rpnnen1lem5  12721  qbtwnre  12933  om2uzlt2i  13671  m1dvdsndvds  16499  pcpremul  16544  pcaddlem  16589  pockthlem  16606  prmreclem6  16622  catidd  17389  ghmf1  18863  gexdvds  19189  sylow1lem1  19203  lt6abl  19496  ablfacrplem  19668  drnginvrn0  20009  issrngd  20121  islssd  20197  znrrg  20773  isphld  20859  cnllycmp  24119  nmhmcn  24283  minveclem7  24599  ioorcl2  24736  itg2seq  24907  dvlip2  25159  mdegmullem  25243  plyco0  25353  sincosq1sgn  25655  sincosq2sgn  25656  logcj  25761  argimgt0  25767  lgseisenlem2  26524  eengtrkg  27354  eengtrkge  27355  ubthlem2  29233  minvecolem7  29245  nmcexi  30388  lnconi  30395  pjnormssi  30530  opsbc2ie  30824  qusvscpbl  31551  naddel1  33839  tan2h  35769  lindsadd  35770  itg2gt0cn  35832  divrngcl  36115  lshpcmp  37002  cdlemk35s  38951  cdlemk39s  38953  cdlemk42  38955  dihlspsnat  39347  isdomn4  40172  clcnvlem  41231  tz6.12i-afv2  44735  sqrtnegnre  44799