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  4599  unielrel  5255  ovmpos  6127  caofrss  6248  caoftrn  6249  f1o2ndf1  6372  nnaord  6653  nnmord  6661  oviec  6786  pmss12g  6820  fiss  7140  pm54.43  7359  ltsopi  7503  lttrsr  7945  ltsosr  7947  aptisr  7962  mulextsr1  7964  axpre-mulext  8071  axltwlin  8210  axlttrn  8211  axltadd  8212  axmulgt0  8214  letr  8225  eqord1  8626  remulext1  8742  mulext1  8755  recexap  8796  prodge0  8997  lt2msq  9029  nnge1  9129  zltp1le  9497  uzss  9739  eluzp1m1  9742  xrletr  10000  ixxssixx  10094  zesq  10875  expcanlem  10932  expcan  10933  nn0opthd  10939  wrdind  11249  wrd2ind  11250  pfxccatin12lem3  11259  maxleast  11719  climshftlemg  11808  dvds1lem  12308  bezoutlemzz  12518  algcvg  12565  eucalgcvga  12575  rpexp12i  12672  crth  12741  pc2dvds  12848  pcmpt  12861  prmpwdvds  12873  1arith  12885  ercpbl  13359  insubm  13513  subginv  13713  rngpropd  13913  dvdsunit  14070  subrgdvds  14193  tgss  14731  neipsm  14822  ssrest  14850  cos11  15521  lgsdir2lem4  15704  gausslemma2dlem1a  15731  m1lgs  15758