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 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  onsucelsucr  4519  unielrel  5168  ovmpos  6012  caofrss  6121  caoftrn  6122  f1o2ndf1  6243  nnaord  6524  nnmord  6532  oviec  6655  pmss12g  6689  fiss  6990  pm54.43  7203  ltsopi  7333  lttrsr  7775  ltsosr  7777  aptisr  7792  mulextsr1  7794  axpre-mulext  7901  axltwlin  8039  axlttrn  8040  axltadd  8041  axmulgt0  8043  letr  8054  eqord1  8454  remulext1  8570  mulext1  8583  recexap  8624  prodge0  8825  lt2msq  8857  nnge1  8956  zltp1le  9321  uzss  9562  eluzp1m1  9565  xrletr  9822  ixxssixx  9916  zesq  10653  expcanlem  10709  expcan  10710  nn0opthd  10716  maxleast  11236  climshftlemg  11324  dvds1lem  11823  bezoutlemzz  12017  algcvg  12062  eucalgcvga  12072  rpexp12i  12169  crth  12238  pc2dvds  12343  pcmpt  12355  prmpwdvds  12367  1arith  12379  ercpbl  12769  insubm  12894  subginv  13073  rngpropd  13207  dvdsunit  13360  subrgdvds  13455  tgss  13859  neipsm  13950  ssrest  13978  cos11  14570  lgsdir2lem4  14728  m1lgs  14748