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  6904  f1imass  7261  focdmex  7953  tposfn2  8246  naddel1  8676  eroveu  8812  sdomel  9122  ackbij1lem16  10236  ltapr  11054  rpnnen1lem5  13031  qbtwnre  13251  om2uzlt2i  14015  m1dvdsndvds  16890  pcpremul  16935  pcaddlem  16980  pockthlem  16997  prmreclem6  17013  catidd  17768  issgrpd  18832  ghmf1  19373  gexdvds  19711  sylow1lem1  19725  lt6abl  20022  ablfacrplem  20194  isdomn4  20877  drnginvrn0  20921  issrngd  21021  islssd  21119  znrrg  21778  isphld  21867  cnllycmp  25184  nmhmcn  25348  minveclem7  25663  ioorcl2  25800  itg2seq  25970  dvlip2  26222  mdegmullem  26303  plyco0  26417  sincosq1sgn  26736  sincosq2sgn  26737  logcj  26843  argimgt0  26849  lgseisenlem2  27612  leadds1im  28252  leadds1  28254  ltonold  28526  onnolt  28531  addonbday  28544  om2noseqlt2  28565  bdaypw2n0bndlem  28728  remulscllem2  28766  eengtrkg  29443  eengtrkge  29444  ubthlem2  31352  minvecolem7  31364  nmcexi  32507  lnconi  32514  pjnormssi  32649  opsbc2ie  32951  qusvscpbl  33791  tan2h  38366  lindsadd  38367  itg2gt0cn  38424  divrngcl  38707  lshpcmp  39861  cdlemk35s  41810  cdlemk39s  41812  cdlemk42  41814  dihlspsnat  42206  clcnvlem  44463  hashnnltb  45846  tz6.12i-afv2  48131  sqrtnegnre  48195