Theorem 3imtr4d 203

Description: More general version of 3imtr4i 201. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses

Ref	Expression
3imtr4d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3imtr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3imtr4d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3imtr4d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	sylibrd 169	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 150	1 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  onsucelsucr  4657  unielrel  5318  ovmpos  6215  caofrss  6338  caoftrn  6339  f1o2ndf1  6468  nnaord  6786  nnmord  6794  oviec  6919  pmss12g  6960  fiss  7316  pm54.43  7542  ltsopi  7693  lttrsr  8135  ltsosr  8137  aptisr  8152  mulextsr1  8154  axpre-mulext  8261  axltwlin  8399  axlttrn  8400  axltadd  8401  axmulgt0  8403  letr  8414  eqord1  8818  remulext1  8935  mulext1  8948  recexap  8989  prodge0  9192  lt2msq  9224  nnge1  9336  zltp1le  9710  uzss  9959  eluzp1m1  9962  xrletr  10227  ixxssixx  10321  zesq  11117  expcanlem  11175  expcan  11176  nn0opthd  11182  wrdind  11516  wrd2ind  11517  pfxccatin12lem3  11526  maxleast  12002  climshftlemg  12093  dvds1lem  12594  bezoutlemzz  12804  algcvg  12851  eucalgcvga  12861  rpexp12i  12959  crth  13031  pc2dvds  13138  pcmpt  13151  prmpwdvds  13163  1arith  13175  ercpbl  13711  insubm  13851  subginv  14043  rngpropd  14361  dvdsunit  14528  subrgdvds  14652  tgss  15289  neipsm  15380  ssrest  15408  cos11  16081  bposlem6  16316  lgsdir2lem4  16355  gausslemma2dlem1a  16382  m1lgs  16409