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  4541  unielrel  5194  ovmpos  6043  caofrss  6159  caoftrn  6160  f1o2ndf1  6283  nnaord  6564  nnmord  6572  oviec  6697  pmss12g  6731  fiss  7038  pm54.43  7252  ltsopi  7382  lttrsr  7824  ltsosr  7826  aptisr  7841  mulextsr1  7843  axpre-mulext  7950  axltwlin  8089  axlttrn  8090  axltadd  8091  axmulgt0  8093  letr  8104  eqord1  8504  remulext1  8620  mulext1  8633  recexap  8674  prodge0  8875  lt2msq  8907  nnge1  9007  zltp1le  9374  uzss  9616  eluzp1m1  9619  xrletr  9877  ixxssixx  9971  zesq  10732  expcanlem  10789  expcan  10790  nn0opthd  10796  maxleast  11360  climshftlemg  11448  dvds1lem  11948  bezoutlemzz  12142  algcvg  12189  eucalgcvga  12199  rpexp12i  12296  crth  12365  pc2dvds  12471  pcmpt  12484  prmpwdvds  12496  1arith  12508  ercpbl  12917  insubm  13060  subginv  13254  rngpropd  13454  dvdsunit  13611  subrgdvds  13734  tgss  14242  neipsm  14333  ssrest  14361  cos11  15029  lgsdir2lem4  15188  gausslemma2dlem1a  15215  m1lgs  15242