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  4655  unielrel  5315  ovmpos  6212  caofrss  6334  caoftrn  6335  f1o2ndf1  6464  nnaord  6782  nnmord  6790  oviec  6915  pmss12g  6956  fiss  7311  pm54.43  7536  ltsopi  7687  lttrsr  8129  ltsosr  8131  aptisr  8146  mulextsr1  8148  axpre-mulext  8255  axltwlin  8393  axlttrn  8394  axltadd  8395  axmulgt0  8397  letr  8408  eqord1  8812  remulext1  8929  mulext1  8942  recexap  8983  prodge0  9186  lt2msq  9218  nnge1  9329  zltp1le  9703  uzss  9952  eluzp1m1  9955  xrletr  10220  ixxssixx  10314  zesq  11109  expcanlem  11167  expcan  11168  nn0opthd  11174  wrdind  11508  wrd2ind  11509  pfxccatin12lem3  11518  maxleast  11994  climshftlemg  12084  dvds1lem  12585  bezoutlemzz  12795  algcvg  12842  eucalgcvga  12852  rpexp12i  12950  crth  13022  pc2dvds  13129  pcmpt  13142  prmpwdvds  13154  1arith  13166  ercpbl  13701  insubm  13841  subginv  14033  rngpropd  14303  dvdsunit  14468  subrgdvds  14592  tgss  15213  neipsm  15304  ssrest  15332  cos11  16004  lgsdir2lem4  16248  gausslemma2dlem1a  16275  m1lgs  16302