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  4545  unielrel  5198  ovmpos  6050  caofrss  6171  caoftrn  6172  f1o2ndf1  6295  nnaord  6576  nnmord  6584  oviec  6709  pmss12g  6743  fiss  7052  pm54.43  7271  ltsopi  7406  lttrsr  7848  ltsosr  7850  aptisr  7865  mulextsr1  7867  axpre-mulext  7974  axltwlin  8113  axlttrn  8114  axltadd  8115  axmulgt0  8117  letr  8128  eqord1  8529  remulext1  8645  mulext1  8658  recexap  8699  prodge0  8900  lt2msq  8932  nnge1  9032  zltp1le  9399  uzss  9641  eluzp1m1  9644  xrletr  9902  ixxssixx  9996  zesq  10769  expcanlem  10826  expcan  10827  nn0opthd  10833  maxleast  11397  climshftlemg  11486  dvds1lem  11986  bezoutlemzz  12196  algcvg  12243  eucalgcvga  12253  rpexp12i  12350  crth  12419  pc2dvds  12526  pcmpt  12539  prmpwdvds  12551  1arith  12563  ercpbl  13035  insubm  13189  subginv  13389  rngpropd  13589  dvdsunit  13746  subrgdvds  13869  tgss  14407  neipsm  14498  ssrest  14526  cos11  15197  lgsdir2lem4  15380  gausslemma2dlem1a  15407  m1lgs  15434